(CoVer) Constraint-based Verification of Reactive systems

Starting date
December 1, 2002
Duration (months)
Computer Science
Managers or local contacts
Giacobazzi Roberto
verification, reactive systems, abstract interpretation, constraints

Reactive systems are ubiquitous computer systems which maintain an ongoing interaction with an external environment, responding with appropriate actions to the external stimuli, and which often perform critical activities such as controlling industrial plants, managing financial transactions, scheduling time-critical operations, running e-commerce and web applications. With the increase of the dependency of our society from computer applications and reactive systems their correct behavior is becoming more and more critical, however their verification is particularly difficult. Practical examples of reactive systems in fact often consists of several sub-components that interact with an environment. Furthermore, their specification may require heterogeneous data and may depend on parameters whose values cannot be fixed a priori. Also, in many cases the set of possible states is infinite. Any of these aspects represents a big obstacle for the applicability of the state-of-the-art verification technology.

The scientific global goal of the project is to use the notion of `constraint', supported by abstract interpretation and type theory, as the unifying concept for the specification and automated verification of complex reactive systems.


Ministero dell'Istruzione dell'Università e della Ricerca
Funds: assigned and managed by the department

Project participants

Matteo Cristani
Associate Professor
Roberto Giacobazzi
Full Professor
Isabella Mastroeni
Associate Professor
Nicola Fausto Spoto
Associate Professor


Research facilities