Overview of techniques for formal Verification of Infinite-State Concurrent systems

Over the last few years there has been an increasing research effort directed towards the automatic formal verification of infinite-state systems. Notable success has been achieved e.g., by the tool UPPAAL. There are now verification techniques for many classes of infinite-state systems, including timed and hybrid automata, petri nets, pushdown systems, systems with FIFO channels, systems with many forms of data structures.

In this tutorial and overview we will survey and present general verification techniques that have been used for infinite-state, and try to show their power and limitations. Such techniques are e.g., symbolic model-checking techniques, abstraction, induction over the networks structure, abstract interpretation, and automata-based techniques.