Next: Verification methods and techniques
Up: Work progress and achievements
Previous: Abstraction and reduction techniques
Algorithmic verification techniques based on
symbolic reachability analysis have been developed for
infinite-state extended automata. More precisely:
- New symbolic representation structures have been developed for the analysis
of models based on automata extended with integer counters
and real valued clocks as well as for models based on timed Petri nets.
- Efficient symbolic state-space exploration procedures have been developed
for various classes of extended automata:
pushdown automata (modeling mutually recursive procedures),
automata with lossy FIFO queues,
counter and clock automata with parametric guards.
Classes of decidable extended automata have been determined, and powerful
fixpoint acceleration techniques have been designed
to help termination of the analysis in the undecidable cases.