Alma universitas studiorum parmensis A.D. 962 - Università di Parma
EUGreen - European University Alliance for sustainability

Event description

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 procedure 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).

Access mode

Live: Ingresso libero fino esaurimento posti
Modified on