Analysis of Systems with Infinite State Spaces

Lecturer: Prof. Javier Esparza (Technische Universität München, Germany).

About the lecturer | Course Summary | Slides and Exercises | Assignment

About the lecturer: Javier Esparza is Professor for Foundations of Software Reliability and Theoretical Computer Science at the Technische Universität München. Previously he held positions in Edinburgh, Munich, and Stuttgart. He has co-authored two books and has published about 100 scientific papers in the fields of automatic program verification, program analysis, and concurrency theory. He has contributed to the theory of Petri nets and to the foundations of program analysis, and has developed model-checking techniques for concurrent, infinite-state, and stochastic systems.

Course summary: In its beginnings, model-checking focused on the analysis of systems with a possibly large but finite state space. However, while the finiteness constraint has proved to be very appropriate for hardware, even the simplest software systems may have an infinite state space. The sources of infinity can be roughly classified into three groups:

In the lectures I will introduce some of the techniques used to automatically verify infinite-state systems. As mathematical models I will present timed automata, broadcast protocols, pushdown systems, and FIFO-automata.

Slides: [PDF]

Assignment: Tasks are here: [PDF]. Due: 27th June. Please send a pdf to Filip Murlak, fmurlak mimuw edu pl.