Modal μ-Calculus for Free
Master Project of Ivan Todorov

Abstract

The process of using formal verification, in order to ensure that a piece of software meets it functional requirements consists of three main steps: designing a model of the given piece of software, translating the functional requirements, which the piece of software must satisfy, into properties of said model and verifying that the model satisfies those properties. Traditionally, regardless of whether the piece of software is developed based on a predesigned model or the piece of software is developed first and its model is designed after that, the piece of software and its model are two separate entities. Therefore, aside from checking that the model satisfies its properties, it must also be verified that the model accurately represents the given piece of software. While this task may initially seem simple, it gets progressively more difficult, as the piece of software becomes more complex. And, if it turns out that the model is not accurate, then the entire formal verification process is invalid, since it does not provide any guarantees about the actual piece of software. In this thesis we present a solution to this problem: a way of modelling sequential effectful programs, such that the resulting models can be directly translated into runnable programs, thereby guaranteeing the models’ accuracy. We achieve this by using algebraic effects, in order to model sequential effectful programs as instances of the coinductive free monad, that could then be translated into runnable pieces of software by applying the necessary effect handlers. Furthermore, we demonstrate that it is possible to express functional requirements as properties of such models using the first-order modal μ-calculus, a fixed-point dynamic logic which has previously been used to reason about labelled transition systems (e.g. in mCRL2).

Thesis

https://repository.tudelft.nl/record/uuid:2c078c39-f60d-4c25-9d0e-35fadd67cc5d