Widening IMPACT

McMillan's IMPACT algorithm showed how abstract models of programs could be refined on demand using interpolants derived from refuting program paths. The algorithm is formulated in terms of unwinding graphs, where each vertex in a graph is a program location paired with a formula that abstracts the state of the program variables at that location. However, the algorithm can generate unwieldy unwinding graphs for some seemingly straightforward programs. Moreover, the graphs can grow without bound, with a run of the algorithm only ending when the memory of the host is depleted. Indeed, IMPACT is a semi-algorithm: it is not guaranteed to complete on all programs to which it is applied. This thesis proposes a novel method to curtail the growth of the unwinding graphs, based on widening (calculating the limits of) formulae at the vertices of the graph.

A program is safe if there is no sequence of states down a branch of a program that leads to an error state. Safety can be observed by showing that there is no sequence of formulae down a branch of the unwinding graph that leads to an error state. Lifting safety from states to formulae provides a vehicle for introducing summaries: a sequence of formulae can summarize many sequences of states since each formula can represent many, possibly infinite, states. The rationale behind IMPACT is to compute sequences of formulae in such a way that one sequence of formulae can be subsumed within another. Subsumption is founded on the concept of covering. Covering is a binary relation on the vertices of an unwinding graph: one vertex covers another if both vertices describe the same program location yet the formula of the former is more relaxed than that of the latter. If all branches emanating from a vertex can be shown to be safe, and the vertex covers another vertex, then there is no need to develop any of the branches at the other vertex.

This thesis develops a new tactic for increasing opportunities for covering sufficient to induce termination. During a run, formulae at vertices often develop in a regular way. These formulae are typically conjuncts of similar subformulae differing by numeric offsets that are strengthened incrementally by adding another subformula (typically on each iteration of a loop). Widening is achieved by representing the conjunctive formula as a universally quantified formula, defined in terms of a variable that ranges over an interval. Then, the interval is relaxed to obtain a stronger formula which corresponds to its limit. Having reached its limit, covering relations, which were previously unstable, hold permanently, allowing IMPACT to terminate.

To represent conjunctive formulae, it is useful to split a formula into two parts: its template and its constants, both of which can be combined to reconstitute the formula. Since the template is stable, it suffices to reason about the n-ary vectors of constants in a formula to derive a summary of the formula. To this end, this thesis introduces a new abstract domain, the march domain, March^n, which summarizes sets of vectors using an interval so as to open up opportunities for widening. This domain is itself constructed compositionally from three subdomains: Int, kInt and Range^n, the latter two of which are also new. The kInt (k-interval) domain represents integers within an interval separated by a multiple, akin to k-bit strided intervals. The Range^n (range) domain represents groups of n-dimensional vectors that all lie on a line which passes through the origin. Once a summary is derived for a set of vectors, it naturally lifts to summarize a set of conjuncts as a single quantified formula. This gives a more compact representation of a formula (which can often be reduced to the first and last conjuncts). The conjunctive formula is widened by dropping a bound on the quantified variable, thereby strengthening the formula.

The novel ideas in this thesis were not developed by pen-and-paper exercises but emerged by exploring multiple runs of IMPACT using a visualization tool called IMPACTEXPLORER, another outcome of this thesis work. The regular conjunctive nature of the formulae, which is key to the whole thesis, would have gone unnoticed if it were not for the development of IMPACTEXPLORER. To conclude, this thesis makes contributions to infinite-state model checking by providing a proof-of-concept demonstrator for extending the IMPACT algorithm with widening.