MoVeMnt: Mode(l)s of Verification and Monitorability
Icelandic Research Fund Project nr. 217987 (January 2021-December 2023)
Status: Ongoing

MoVeMnt is a 3-year project funded by the Icelandic Research Fund, starting in 2021. The project is led by Luca Aceto (Reykjavik University and Gran Sasso Science Institute), Antonis Achilleos (Reykjavik University), Adrian Francalanza (University of Malta), Anna Ingolfsdottir (Reykjavik University), and Karoliina Lehtinen (Aix-Marseille University) It continues work from the TheoFoMon project. The aims of MoVeMnt are to:

Researchers

The research team includes, in alphabetical order, Luca Aceto (Reykjavik University and Gran Sasso Science Institute, co-PI), Antonis Achilleos (Reykjavik University, PI), Elli Anastasiadi (PhD student at Reykjavik University), Duncan Paul Attard (PhD student at the University of Malta and at Reykjavik University), Leo Exibard (Reykjavik University, postdoctoral researcher), Adrian Francalanza (University of Malta, co-PI), Anna Ingolfsdottir (Reykjavik University, co-PI), Karoliina Lehtinen (Aix-Marseille University, co-PI), Mathias Ruggaard Pedersen (Reykjavik University, postdoctoral researcher), Shabnam Rahimi (Reykjavik University, MSc student), and Jasmine Xuereb (PhD student at the University of Malta and at Reykjavik University).

Project-related events (in reverse chronological order)

Publications

Journal papers

  1. L. Aceto, A. Achilleos, E. Anastasiadi and A. Ingolfsdottir. Axiomatizing recursion-free, regular monitors. Journal of Logical and Algebraic Methods in Programming, special issue devoted to selected papers from NWPT 2019, 2022. To appear. [Publisher's version] [Author's preprint]

Conference and workshop papers

  1. Leo Exibard, Emmanuel Filiot, Ayrat Khalimov. A Generic Solution to Register-bounded Synthesis with an Application to Discrete Orders. To appear in ICALP 2022. [arxiv]
  2. Antonis Achilleos, Léo Exibard, Adrian Francalanza, Karoliina Lehtinen and Jasmine Xuereb. A Synthesis Tool for Optimal Monitors in a Branching-Time Setting. Tool paper, in COORDINATION 2022. [author preprint version]
  3. Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza and Anna Ingolfsdottir A Monitoring Tool for the Linear-Time μHML. Tool paper, in COORDINATION 2022 (best paper award for COORDINATION and for DisCoTec 2022!). [author preprint version]
  4. Elli Anastasiadi, Antonis Achilleos and Adrian Francalanza. Monitoring Hyperproperties with Circuits. Short paper, in FORTE 2022. [author preprint version]
  5. Luca Aceto and Anna Ingolfsdottir. Introducing Formal Methods to First-Year Students in Three Intensive Weeks. Proceedings of Formal Methods Teaching, FMTea21 (Ferreira J.F., Mendes A. and Menghi C. eds.), Lecture Notes in Computer Science 13122, pp. 1-17, Springer, November 2021. [Publisher's version] [Publicly accessible version]
  6. Duncan Paul Attard, Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen: Better Late Than Never or: Verifying Asynchronous Components at Runtime. DisCoTec 2021. [available on HAL]
  7. Antonis Achilleos and Mathias Ruggaard Pedersen: Axiomatizations and Computability of Weighted Monadic Second-Order Logic. LICS 2021. [available on arxiv]

Other publications

  1. Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Leo Exibard, Adrian Francalanza, Karoliina Lehtinen. Runtime monitoring for Hennessy-Milner logic with recursion over systems with data.. To be presented at the Logic Colloquium 2022.
  2. Antonis Achilleos, Eleni Bakali, Aggeliki Chalki, Aris Pagourtzis. The complexity for hard counting problems with easy decision version. To be presented at the Logic Colloquium 2022.
  3. Antonis Achilleos, Elli Anastasiadi, Adrian Francalanza, Karoliina Lehtinen and Mathias Ruggaard Pedersen. On Probabilistic Monitorability. To appear.

Submitted papers

  1. Elli Anastasiadi, Antonis Achilleos, Adrian Francalanza and Jasmine Xuereb. Epistemic logic for verifying runtime verification communication protocols.
  2. Luca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir. Bidirectional Runtime Enforcement of First-Order Branching-Time Properties. [available on arxiv]

Software tools

  1. DetectEr, an RV to synthesise montors for branching-time and linear-time recHML properties.
  2. A Synthesis Tool for Optimal Monitors in a Branching-Time Setting