There is a recent trend toward the automation of the model checking and computer program verification process. The program or the model being verified and its verifiable property need to be restricted in the finite state spaces. The authors address the set-based reduction method for automatic computer program verification.

The authors develop two methods of implementing state matching: one using quantifiers and another that is quantifier-free. The authors use two case studies to investigate the relationship between image-based and equivalence-based state matching, namely DVE (native language of DIVINE) models and random models. Further, the authors employ the DVE language for open systems, set-based reduction with explicit sets, set-based reduction with symbolic sets, equivalence-based versus image-based state matching and image versus equivalence using linear search, and experiments with witness-based matching resolution in both DVE and random models.

The authors claim the novelty of their method lies in “the combination of explicit-state model checking with sets of variable evaluations represented as images of bit-vector functions.” They further observe that explicit model checking made it possible to verify programs with nontrivial data flow. For future enhancements, the authors suggest “precisely distinguish[ing] between the sets of variable evaluations” and improving program verification using counterexample guided refinement, loop acceleration, and a compositional approach to control flow.

This paper is an interesting read for those who are working in the area of explicit-state model checking and computer program verification. The authors affirm that “the ability to produce counterexamples is a crucial property of linear temporal logic model checking,” which makes this paper worth reading.