MoVeMnt

Mode(l)s of Verification and Monitorability

New page here!


MoVeMnt is a 3-year project funded by the Icelandic Research Fund, starting in 2021. It continues work from the TheoFoMon project.

The aims of MoVeMnt are to:

  • Examine the monitorability of hyperproperties. Besides the properties of a single execution or of the whole system, hyperproperties, which are properties of sets of traces, are a reasonable model for the execution of a system that may be distributed, or run several times.

  • Study monitors that give verdicts equipped with structure. That structure can be used to justify a conclusion, alter an execution trace, or extract a quantity from the system run, instead of simply giving a binary answer.

  • Determine the decidability and complexity of the monitorability of a property.

  • Assess the abilities of monitors that use more computational resources than regular monitors, such as various types of memory or clocks.

  • Find effective ways to combine different verification techniques to mitigate their respective limitations and verify a specification in the most appropriate manner.

  • Compare monitorability with other important and related techniques, such as learning and diagnosability.


The project's coPIs from Reykjavik University are Antonis Achilleos, Luca Aceto, and Anna Ingólfsdóttir. From outside RU, the ptoject has two co-proposers, Adrian Francalanza from the University of Malta, and Karoliina Lehtinen from LIS, Aix-Marseille.