Abstraction and reduction techniques

1. Abstraction techniques have been developed in order to verify (safety and liveness properties) of classes of infinite-state systems such as (1) systems manipulating data ranging over infinite domains, and (2) parametrized networks with an arbitrary number of components.
2. Abstraction refinement techniques, based on the analysis of counter-examples, have been developed for use in automatic design of accurate abstraction relations.
3. Static analysis techniques, such as live variable analysis and program slicing, have been developed and used as model reduction techniques in the framework of the validation (verification and test case generation) of real industrial case studies.
4. Reduction techniques and efficient state exploration techniques based on Petri nets unfoldings have been developed and used for model-checking.