The authors discuss the automatic analysis and verification of concurrent programs with unbounded integer variables. These programs are expressed in the event-action language and have their semantics defined in terms of infinite (because of unbounded integer variables) transition systems. The characterization of the states and the specification of the transitions are expressed as Presburger formulas (affine constraints over integer variables). The temporal properties targeted for verification are expressed in concurrent temporal logic (CTL) built over Presburger state formulas.

The essence of the paper is in taming the complexity of the verification proofs. The restriction to Presburger formulas and the use of existing efficient solvers is but one factor. In addition, two approaches are used: abstraction of the infinite state systems, thus reducing their size, and approximation analysis leading to shorter and simpler proofs. The abstraction consists of partitioning the infinite space by identifying clusters of values with “equivalent” behavior. Three complementary techniques for partitioning the space are discussed. When the abstraction is not sufficient to lead to efficient exact analysis, approximation is used to compute upper and lower bounds using the widening technique. The authors illustrate their approach on a simple running example. Additional examples are discussed.

The paper is 42 pages long, divided into nine sections. Its length is explained in part by the fact that it is very well motivated and explained. I found it to be self-contained and easy to read. The first sections position the paper with respect to previous work. While it builds on previous work by others, all concepts used in the paper are introduced and thoroughly explained. I would have liked to see a discussion of the applicability of this approach to the analysis of active database models.