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
|