The problem of automatic verification of programs is a grave one, even for “small” programs, since their semantic models grow not only with the size of the program, but also with the number of variables and the size of the variables’ domains. Static tools extract information on the semantics of the program without creating a semantic model.

In this paper, Yorav and Grumberg propose two orthogonal reduction models to maintain the state-explosion problem for the automatic verification of sequential and parallel programs. The first model compresses the computational paths (path reduction), and the second reduces the dead variables. The process creates a reduced transition system as a model of the program, on which verification tools can then act. The specifications considered in this work are formulas of the CTL* and CTL-X* logic.

Since the approach is based on syntactic manipulations of expressions, it is applicable when dealing with variables of both finite and infinite domains. The simulation study reveals the promise of this approach, especially in parallel program verification.

The paper is written in a legible, easy to follow style, and the material is laid out methodologically. The text is self-contained to a degree; it provides a good overview of related work, the problems, and the motivation for the work, as well as a plethora of proofs for the claims made. The experimental results support the outlined theory well.