Formal methods for concurrent systems

The activities of the group in asynchronous systems a valuable experience in formal methods for concurrent system. Petri nets were the main design paradigm for the specification, synthesis and verification of asynchronous systems.

The research in this area is mainly devoted to study and propose algorithms for the verification of concurrent systems. In particular, models for the interaction of reactive systems, algorithms for the verification of timed systems and Petri net synthesis techniques are some of the topics we are studying. The paradigm of abstract interpretation is one of the main resorts we are now using to tackle the complexity of the verification problems.

As an example of our research, you can have a look of a paper that proposes a new domain for abstract interpretation:

R. Clarisó and J. Cortadella,
The Octahedron Abstract Domain,
11th Static Analysis Symposium (SAS), Verona, August 2004. [PDF]

Back to GAVINA group