Automated Support for the Design and Validation of Parameterized Systems

The main and final goal of this project is to provide an automatic tool to support the design and validation of parameterized systems. This page is a collection of a series of single projects focusing on an extension of the infinite-state model-checker SAFARI, required either to gain a speed-up in solving certain tasks or for defining new solutions.

The increasing complexity of engineered systems makes verification processes a fundamental stage in software and hardware development. Nowadays, more and more distributed systems are applied in many heterogeneous field (sensors networks, e-commerce, distributed databases, real-time systems, mission-critical systems). One main feature distinguishes them from single-thread systems: their being parameterized in the number of the agents acting in their execution. Think about an operating system with many users, a database running on many servers, a protocol involving several processes: all these systems have to be verified keeping unknown the number of these agents. This feature makes classical formal verification technologies unsuitable for the verification of parameterized systems, because they requires to work with a system with a finite number of possible configurations, while the unknown number of agents makes the number of configurations unknown, hence potentially unbounded.
This problem is, in its general formulation, undecidable; however it has been shown that if the system under verification met certain hypotesis, a sound solution exists (solution that is also complete for a more restrictive class of hypotesis). This solution relies on the computational power of an infinite-state model-checker.

Goal(s) of the project

The main and final goal of this project is to provide an automatic tool to support the design and validation of parameterized systems such as multi-thread programs, cache coherence, mutual exclusion and fault-tolerant protocols, procedures handling unbounded data structures, etc.
The solution will exploit SAFARI, an infinite-state model-checker. SAFARI is highly modular and still growing. Students will work on a new module with the supervision (and support) of Francesco Alberti, SAFARI's main developer and maintainer ( and Prof. Natasha Sharygina (
Possible extensions include, but are not limited to, the following:
- search of invariants. This module will help in gaining a global speed-up in the verification of systems.
- elimination of quantifiers. This feature helps in purifying configurations and extends SAFARI towards the verification of hybrid and/or real-time systems.
- verification of liveness properties. Verification of liveness properties can be reduced to the verification of a set of safety properties.
- Integration of SAFARI with other tools used in verification as an invariant generator.

Required skills

- Good knowledge of C++ 
- Previous knowledge in verification/formal methods is a plus

Acquired competencies

- Knowledge about problems arising in formal verification of parameterized systems
- Knowledge in formal methods applied to the verification
- Practical application of theoretical notions into efficient, useful, and practical tool