Résumé: Software model checking is the algorithmic analysis of programs to prove properties of their executions. It traces its roots to logic and theorem proving, both to provide the conceptual framework in which to formalize the fundamental questions and to provide algorithmic procedures for the analysis of logical questions. The undecidability theorem [Turing 1936] ruled out the possibility of a sound and complete algorithmic solution for any sufficiently powerful programming model, and even under restrictions (such as finite state spaces), the correctness problem remained computationally intractable. However, just because a problem is hard does not mean it never appears in practice. Also, just because the general problem is undecidable does not imply that specific instances of the problem will also be hard. As the complexity of software systems grew, so did the need for some reasoning mechanism about correct behavior. (While we focus here on analyzing the behavior of mechanisms happened in parallel, and merits a different survey.) Initially, the focus of program verification research was on manual reasoning, and the development of axiomatic semantics and logics for reasoning about programs provided a means to treat programs as logical objects [Floyd 1967; Hoare 1969; Dijkstra 1976; Apt and Olderog 1991]. As the size of software systems grew, the burden of providing entire manual proofs became too cumbersome, and brought into questions whether long and laborious proofs of correctness could themselves be trusted [de Millo et al. 1979]. This marked a trend toward automating the more mundane parts, leaving the human to provide guidance to an automatic tool (for example, through loop invariants and function pre- and post-conditions [Dijkstra 1976]). This trend has continued since: the goal of software model checking research is to expand the scope of automated techniques for program reasoning, both in the scale of programs handled and in the richness of properties that can be checked, reducing the burden on the expert humanprogrammer. More recently, software model checking has been influenced by three parallel but somewhat distinct developments. First, development of program logics and associated decision procedures [Nelson 1981; Nelson and Oppen 1980; Shostak 1984] provided a framework and basic algorithmic tools to reason about infinite state spaces. Second, automatic model checking techniques [Clarke and Emerson 1981; Queille and Sifakis 1981; Vardi andWolper 1994] for temporal logics [Pnueli 1977; Emerson 1990] provided basic algorithmic tools for state-space exploration. Third, compiler analysis, formalized by abstract interpretation, provided connections between the logical world of infinite state spaces and the algorithmic world of finite representations. Throughout the 1980s and 1990s, the three communities developed with only occasional interactions. However, in the last decade, there has been a convergence in the research directions and modern software model checkers are a culmination of ideas that combine and perhaps supersede each area alone. In particular, the term "software model checker" is probably a misnomer, since modern tools simultaneously perform analyses traditionally classified as theorem proving, or model checking, or dataflow analysis. We retain the term solely to reflect historical development. In this survey, we trace some of these ideas that have combined to produce tools with more and more automation and precision for the analysis of software systems.

Langue: Anglais