Research | Formal Methods for the Verification and Synthesis of Systems

Realizing digital systems has never been an easy task and nowadays has become even more difficult due a considerable increase of their complexity. In this context, the development of methodologies for the automatic synthesis of correct systems (synthesis) or to check that a system fulfils some correctness requirements is relevant. Several methodologies have been developed that in many cases have produced industrial success. In particular, the techniques that are developed within robust mathematical theories can benefit of a series of tools and results that can facilitate the design, implementation and validation of the synthesis and verification tools themselves. Another important feature of these methodologies is that they may operate on an abstract model of the system and thus can be used in advanced compared to other techniques such as testing and simulation.

The competencies of the members of the “Automatic Verification and Synthesis” research group at the Dipartimento di Informatica cover both practical and theoretical aspects of model-checking. The research contributions of the last years have concerned with both the study of the theoretical foundations, and the development and implementation of new methodologies for the verification and synthesis of sequential and concurrent programs, (parametric) real-time and hybrid systems, open and modular systems. Besides the advantages of the other formal methods, model-checking is fully automatic and in case a specification is violated it yields a counter-example that allows a fast identification of the error.

Research topics

• Model-checking
• Concurrent program verification
• Embedded system verification
• Real-time and hybrid system verification
• Multicore verification
• Bounded model checking
• Automatic generation of test cases
• Automata theory
• Temporal logic
• Game graphs
• Computational complexity
• Models of concurrency