The code of a procedural-language computer program includes variables that have values at any given point during execution of that program. The state at a point of execution of a program includes the collection of values of all variables at that point. One (by now) time-honored formal, that is, rigorous, mathematical method of program verification is model checking [1], wherein the states of a program are examined for correctness (fidelity to purpose and design) and for other desirable properties such as soundness. For example, if Boolean variable b actuates an automobile’s brakes at time t, then the acceleration-actuator output-variable a should be verified as having the value “false” at that instant. It is arguably obvious that the number of states of a program of even moderate size is astronomic, and that full state matching comprises a brute-force, exhaustive approach that is of limited practicality.

Partial state matching, the general subject of this 27-page paper, is an approach to taming this combinatorial explosion of states. The more specific subject is the technique of dead variable reduction (DVR). By way of intuitive definition, “a variable v that is dead at program point p can be ignored” [2]; that is, dead variable v need not appear in the table of program states at point p, nor need its value be checked there. Execution paths and threads that include dead variables can analogously be excluded [2]. This paper has a further specialization of scope, namely the inclusion of variables and data residing in heap storage: “Involving their consideration in DVR can further improve the state-matching performance.”

Included in the introductory background section of the paper is a multiple-thread Java example that immediately, and very efficiently, illustrates the specific content of the paper: equivalent data structures, here trees, one of which is DVR-reduced. (The caption for Figure 1 should refer to “two threads,” that is, in the plural.) State matching is subsequently explicated via the authors’ dynamic dead variable analysis (DDVA), wherein a reduced state vector (of visited states) is computed and stored along with the live addresses. The authors’ complementary hybrid analysis (HybridDVA) “targets scalability and speed.” This analysis begins with pre-model-checking static analysis, and is followed by call-stack analysis of functions (or Java methods). Variables (also known as “fields”) are marked as live and “only these are considered in state matching.”

Section 4 explicates formalization of the preceding notions, this in clear notation. Though this paper must be classified as quite advanced and aimed at experts, any reader will appreciate, for example, the proof-sketch that precedes the proof of the bisimulation theorem (the relation among states).

Section 5 describes implementation (in JavaPathFinder, JPF), and displays algorithms in clear pseudocode (including the “classical” baseline, and that with the authors’ extensions). The discussion of Java’s heap storage, and how (D)DVA and HybridDVA relate thereto, is deep, detailed, and productive of insight. The section on Java Virtual Machine (JVM) bytecode is equally detailed and refined.

Table 5 summarizes experimental results for the number of states and running times for JPF, JPF with hybrid DVR, and JPF with dynamic DVR for various benchmarks, such as AlarmClock, Elevator, and ProdConsumer. Table 6 does the same for memory consumption. The objective of the experiments was to determine “whether and to which extent the DVRs improve the performance of software model checking in . . . Java PathFinder.” I gave both tables more than glancing perusal, and was quite appreciative of the authors’ summary section: “The results of the benchmarks demonstrate that the contribution to performance in both the hybrid and dynamic DVR cases is significant.” One also has to agree that the reduction in memory consumption engendered by the use of the authors’ DVRs is “especially valuable,” given that the most frequent failure of model checking is insufficient available memory.

This paper is significant in several ways: it is deep with respect both to theory and experiment, and is explicit both in the premises of its formalism and in the Java infrastructure over which its model checking is done. It has certainly made the case of dead variable analysis and reduction in rendering model checking increasingly practical. I recommend the paper highly.