On Dec 9, 2024 I will be giving an invited seminar at University of Parma, Italy.

Abstract of the seminar:

Model checking is a formal technique to assess the correctness of systems by exhaustively searching its state space for “bad” executions. If no such execution is found, the system is safe. Otherwise, the execution is called a counterexample and shown to the user, who may use it to debug the system (or refine their definition of “bad”). Today, model checking is routinely used in hardware design, and has seen increasing adoption in the software domain as well. This required a number of theoretical breakthroughs, due to the large state spaces that even modest programs exhibit. This seminar will provide an overview of model checking approaches to software verification. We will start from the basics and then discuss a few more advanced procedures that have been devised to tackle programs with large (or infinite) state spaces. Lastly, we show how these solutions may also enable automated reasoning on “complex adaptive systems”. These are collections of autonomous, interacting agents which may display emergent collective behaviour (think about flocks of birds or colonies of ants).

Many thanks to Vincenzo Arceri for inviting me!

Update: Slides from the seminar are available here.