Spring 2021

Course Description

Model checking and related techniques of automatic formal verification emerged in the early 1980’s. These methods present a cost and a benefit: we must model our system and write our specification in very restricted forms, but in exchange for this we obtain proofs and counterexamples automatically. Despite early successes, this approach immediately led to difficult problems, for example, how to extend the expressiveness of the models to allow the verification of real systems, while keeping the proofs tractable. The model checking paradigm is the collection of strategies that researchers developed for resolving these problems.

The class will survey a sampling of research topics within the model checking paradigm, with a view to elucidating the high-level strategies, while disregarding algorithmic details. In this way, we will try to make some sense of the diverse and not always coherent literature in the field. The goal is for students to be able to read critically and put into context recent papers in areas such as software model checking, cyber-physical systems or neural network verification.