This page provides material for a course on configurable software model checking, given at the RiSE/SHiNE Winter School 2018, February 5-9, 2018, TU Wien, Vienna, Austria.
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. The second part illustrates concepts like cartesian and boolean abstraction, lazy abstraction, CEGAR, and interpolation on the example of the software model checker BLAST. The third 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. The fourth part focuses on practical aspects of software model checking and explains approaches like conditional model checking, regression verification, and witness-based result validation.