We give an overview of the development of software model checking, a general approach to algorithmic program verification that integrates static analysis, model checking, and deduction. We start with a look backwards and briefly cover some of the important steps in the past decades. The general approach has become a research topic on its own, with a wide range of tools that are based on the approach. Therefore, we discuss the maturity of the research area of software model checking in terms of looking at competitions, at citations, and most importantly, at the tools that were build in this area: we count 76 verification systems for software written in C or Java. We conclude that software model checking has quickly grown to a significant field of research with a high impact on current research directions and tools in software verification.

This talk is based on the following joint work with Andreas Podelski: https://doi.org/10.1007/978-3-031-22337-2_27

Presentation slides: https://www.sosy-lab.org/research/prs/2023-09-11_CPAcheckerWS23_SoftwareModelChecking_Dirk.pdf

Dirk Beyer is Professor of Computer Science and has a Research Chair for Software Systems at LMU Munich, Germany. He was Full Professor at University of Passau (2009-2016), Assistant and Associate Professor at Simon Fraser University, B.C., Canada, and Postdoctoral Researcher at EPFL in Lausanne, Switzerland (2004-2006) and at the University of California, Berkeley, USA (2003-2004) in the group of Tom Henzinger. Dirk Beyer holds a Dipl.-Inf. degree (1998) and a Dr. rer. nat. degree (2002) in Computer Science from the Brandenburg University of Technology in Cottbus, Germany. In 1998 he was Software Engineer with Siemens AG, SBS Dept. Major Projects in Dresden, Germany. His research focuses on models, algorithms, and tools for the construction and analysis of reliable software systems. He is the architect, designer, and implementor of several successful tools. For example, CrocoPat is the first efficient interpreter for relational programming, CCVisu is a successful tool for visual clustering, and CPAchecker and BLAST are two well-known and successful software model checkers.