# iFM^{2}

informal Formal Methods Meetings

iFM^{2} is a series of informal talks held at the University of Udine on everything about Formal Methods. The series has seen a great number of talks from people all around Italy and beyond. Here you find the slides for almost all the talks held so far.

#### Upcoming

Department of Mathematics, Computer Science and Physics

"Sala Riunioni" (II floor)

###### Abstract

Runtime verification consists in checking whether a program satisfies a given specification by observing the trace it produces during its execution. It is used as a lightweight verification technique to complement or substitute costlier methods such as model-checking. In the regular setting, Hennessy-Milner logic with recursion (recHML), a variant of the modal mu-calculus, provides a versatile back-end for expressing linear- and branching-time specifications of the control flow of the system.

In this talk, I will discuss an extension of this logic that allows to shift the focus from control to data and express properties over the data values (i.e. values from an infinite domain) manipulated by the system. and examine which fragments can be verified at runtime. Data values are manipulated through equality tests in modalities and through first-order quantification outside of them. They can also be stored using parameterised recursion variables.

I then examine what kind of properties can be monitored at runtime, depending on the monitor model. A key aspect is that the logic has close links with register automata with non-deterministic reassignment, which yields a monitor synthesis algorithm, and allows to derive impossibility results. In particular, contrary to the regular case, restricting to deterministic monitors strictly reduces the set of monitorable properties. I then conclude by examining whether we can delineate a maximally monitorable fragment for the logic, and the picture turns out to be quite intriguing.

This is joint work with the MoVeMnt team (Reykjavik University): Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Adrian Francalanza, Karoliina Lehtinen.