Although it is perhaps the worst of times to bring up investment advice or financial planning as an example, I’ve always been amused when asked about my investment goals. The impulse answer is to gain the highest return, in the shortest time, and in the safest manner. An analogy with system and software design presents itself: I want to design the software in such a way that it performs its required functions correctly. My point is that correctness has become widely regarded as an attribute--along with, say, size and speed of execution--and has, as such, evolved into something that seems negotiable: “it’s not a bug, it’s a feature.” There have even been suggestions, with which I vehemently disagree, that to be overly concerned with correctness stifles software design creativity [1].

There are, broadly speaking, two formal methodologies for assessing or ensuring correctness: theorem proving as, for instance, in the B-Method [2] and model checking [3], which is performed by using model checkers such as SPIN, the subject of this authoritative compendium on its state of the art and practice. (The predictable hybridization of the two paradigms is proceeding apace.)

This very advanced volume in Springer’s “Lecture Notes in Computer Science (LNCS)” series comprises the proceedings of the 15th International SPIN Workshop. In case you are not familiar with this series, you should know that the term “lecture notes” should be broadly interpreted. SPIN is indeed the unifying theme, but the papers are, inevitably, more loosely coupled than they would be in a single lecturer’s sections and chapters. This is not a criticism, but only a cautionary comment. Many of the individual papers--a randomly chosen example is Fecher and Shoham’s “State focusing: lazy abstraction for the mu-calculus”--certainly qualify as mini lecture notes, with multiple rigorous definitions and precise displays of algorithms. Others lean more toward excellent, peer-reviewed journal papers (true of all contributions), with less tutorial content.

Prior to the breakthrough for which Clarke, Emerson, and Sifakis received the 2007 Turing Award, model checking was a brute force enterprise that was hobbled by the combinatorial explosion that characterizes evaluation of large truth tables in the search for tautologies or counterexamples in (what amounts to) the Boolean equations that specify a system. The breakthrough enabled beneficial proliferation of model checking applications that are beginning to show, collectively, a way to tame the correctness monster for real-life sequential, concurrent, and distributed systems. The SPIN model checker is the brainchild of G.J. Holzmann, who is the coauthor of one of the book’s papers, and who sat on the program and advisory committees of this workshop. Holzmann gave us a preview of SPIN, along with its PROMELA language, in the early 1990s, at a software process improvement network (also SPIN) meeting at Rutgers University.

Four “invited contributions,” totaling 25 pages, begin these proceedings; these are followed by 18 “regular papers” that collectively span over 300 pages. It is safe to characterize the entire volume as written by experts for an audience of professionals--would-be or otherwise--in the model checking subspecialty of computing science and practice. Interested fellow travelers are those who do not consider correctness optional, such as those who create or purvey safety-critical, security-critical, trusted, or any other high-assurance systems that are based on discrete logic, the latter including software, firmware, and hardware; the last is treated in the book, in Singh and Shukla’s paper.

Section 2 of Dwyer and Purandare’s paper, “Residual checking of safety properties,” sets an apposite tone for the entire proceedings, which later seem to cover all of the theory underlying contemporary model checking, using SPIN and PROMELA as instantiation and implementation. Topics covered in the first half of the remaining 21 papers include: context-bounded verification; program properties via static and dynamic reasoning; dynamic symbolic execution; checking abstract components in concrete environments; probabilistic model checking; and bounded model checking of concurrent systems.

The second half of the book begins with Holzmann, Joshi, and Groce’s “Tackling large verification problems with the Swarm tool.” Subsequent topics include: device driver verification experience, with its welcome instance of data abstraction (the great enabler of model checking); dependency analysis; Boolean equations used for on-the-fly equivalence checking; randomized large-state-space exploration for verification; state model checking via incremental hashing as a generalization of Karp and Rabin’s recursive hashing; multithreaded Java programs; and symbolic string verification.

This extraordinarily well-composed book belongs in every research library. By perusing these proceedings, beginners will also be able to appreciate the breadth and depth of this exciting field.