The courses Model Checking I and Automata, languages, and computability are convenient to follow the course, but not indispensable. In particular, at the beginning of the course basic ideas from automata theory will be recalled.

Model-checking is a technique for the automatic verification of the correctness of hardware and software systems. Until the middle 90s model checking focused mostly on the analysis of systems with a possibly large but finite state space. Model checking techniques for finite state systems are studied in the Wahlpflichtvorlesung Model Checking I.

While the finiteness constraint has proved to be very appropriate for hardware, even very simple software systems may have an infinite state space. The sources of infinity can be roughly classified into three groups:

1. Control: (possibly recursive) procedures and process creation require to enrich the notion of state with unbounded stacks or sets.
2. Data: the use of any datatype with an infinite range, like integers, reals, lists, queues, etc. potentially leads to an infinite state space.
3. Parameterization: distributed algorithms (like algorithms for mutual exclusion, leader election, byzantine agreement, etc.) are often designed to work for an arbitrary number of processes, i.e., a distributed algorithm is in fact an infinite infinite family of systems. Checking that all elements of the family satisfy a property can be reduced to checking that one single infinite-state system satisfies it.

The last decade has shown that many of these infinities can be tamed by applying some rather elementary but fascinating ideas from mathematics, combined with clever algorithmic techniques from computer science. This has lead to software tools for checking and optimizing software systems which are currently finding their way into the software industry.

In the lectures I will introduce some of the techniques used to obtain verification algorithms in the infinite-state case. I will consider four classes of systems: timed automata, broadcast protocols, pushdown systems, and FIFO-automata. For each class we will try to cover the spectrum from basic theory to concrete applications, and where applicable also to software tools.

There is a set of slides for the course. Additional material will be distributed along the course during the lectures.

The course is based on the following papers:

• R. Alur, D.L. Dill: A Theory of Timed Automata. Theoretical Computer Science 126(2): 183-235 (1994)
• J. Esparza, A. Finkel, R. Mayr: On the Verification of Broadcast Protocols. Proc. of LICS 1999 (1999)
• J. Esparza, D. Hansel, P. Rossmanith, S. Schwoon: Efficient Algorithms for Model Checking Pushdown Systems. Proc. of CAV 2000 (2000)
• A. Vardhan, K. Sen, M.Viswanathan, G. Agha: Actively Learning to Verify Safety for FIFO Automata. Proc. of FSTTCS 2004 (2004)