This page provides material for a course on configurable software model checking, given at the Eighth Summer School on Formal Techniques, May 19 - May 25, 2018, Menlo College, Atherton, CA.
The goal of this lecture is to bridge the gap between verification research and software engineering. Consequently, the lecture starts with theory and concepts, continues with a unifying view on several different verification algorithms, and finally addresses some practical problems that occur in software verification. The first part gives an introduction of the framework of configurable program analysis and shows how state-of-the-art concepts like cartesian and boolean abstraction, lazy abstraction, CEGAR, interpolation, and large-block encoding can be integrated in a configurable way. The second part consolidates knowledge and we show how to express the four different ``schools of thought'' of software verification in one unifying framework: bounded model checking, k-induction, predicate abstraction, and lazy abstraction with interpolants. We also shed light on practical aspects of software model checking and explain approaches like regression verification, witness-based result validation, conditional model checking, and reducer-based verification.