Verification of infinite state systems

Course outline: 

In this course, we will give an overview of some fundamental problems and classical techniques in the automated verification of infinite state systems.
The problems we will mainly focus on are the so-called satisfiability and model checking problems for formulas of first-order logic and monadic second-order logic, as well as variants of the reachability problem on pushdown automata and Petri nets. We will begin by recalling the fundamental results by Büchi and Rabin showing the decidability of monadic second-order theories of structures with one and two successors. We will then present application examples and techniques such as composition method, logical interpretation, unfolding, fixpoint computation of reachable sets.