Special section on the algorithmics of software model checking — Introductory paper

The term “software model checking” has recently been coined to refer to a flourishing area of research in software verification – the formal, automated analysis of program source code. Software model checking is considered an important application of classical model checking, where the model of a software system is analyzed in an automated fashion for compliance with a property specification. While classical model checking assumes the existence of an abstract model of the software system to be analyzed, in software model checking the emphasis is on directly analyzing program code given in a standard programming language, such as Java or C. This introduces a variety of significant obstacles, chief among them the efficient treatment of the complex data, e.g., heap structured data, and control constructs, e.g., procedure calls and exception handling, found in modern programming languages. These obstacles can also be viewed as opportunities for adapting traditional model checking data structures and algorithms to exploit the particular semantics of programming language constructs to gain improved performance. Moreover, while classical model checking emphasizes proving a model correct as the primary objective, an increasingly widely held view is that model checkers can function effectively as anomaly detectors or bug finders, i.e., they locate and explain undesired behavior of the software. This special section is the second devoted to publishing revised versions of contributions first presented at the International SPIN Workshop Series on Model Checking Software. In recent years this series of workshops has broadened its scope from focusing on the model checker SPIN to covering software model checking technology in general. The editorial introduction by Havelund and Visser to the first STTT special section devoted to SPIN papers [11] provides an excellent overview of the foundational ideas underlying software model checking. That special section was based on papers presented at the 7th International SPIN Workshop held at Stanford University (USA) in August/September 2001. Authors of well-regarded papers from the 8th International SPIN Workshop held in Toronto (Canada), colocated with ICSE 2001 on May 10–11, 2001, and the 9th International SPIN Workshop on Model Checking Software, held April 11–13, 2002 in Grenoble (France) as a satellite event of ETAPS 2002,were invited to submit to this special issue. All three of the papers included here have been extended to include significant new content and have undergone an independent round of reviewing