Predicate Abstraction

Predicate abstraction is a technique that is used to prove properties of infinite state systems. It is a combination of theorem proving and model checking techniques. Given a concrete infinite state system and a set of abstraction predicates, a conservative finite state abstraction is generated. It is conservative in the sense that for every execution in the concrete system there is a corresponding execution in the abstract system. The abstract version of the verification condition is model checked in this abstract system. If the property is verified then it holds in the concrete system. Otherwise an abstract counter-example trace is generated. There could be a concrete counter-example corresponding to it, in which case there is a bug in the design, or the abstract counter-example is an artifact of the abstraction. Our tool can automatically analyze the counter-example to find a real bug or to suggest extra predicates to refine the abstraction thereby avoiding that particular spurious trace. Then the process starts anew. This process is not guaranteed to terminate, after all proving arbitrary safety properties of an infinite state system is not decidable, but for a large number of problems this method can successfully prove properties.

Computing the abstract transition relation can be expensive. So at first we compute an approximate abstract transition relation. If the abstract verification condition can be proved with this approximate system, then we don't need to carry out further computation. Otherwise we check if every step of the abstract counter-example trace is allowed in the exact abstract transition relation. If that is the case then we have found an abstract trace and we don't need a more accurate transition relation. Otherwise a constraint is added to the abstract transition relation and the property model checked again in the more accurate approximation.

The complete process is described in the following diagram. Notice that there are two nested loops. In the inner loop the predicates used remain the same while the abstract transition relation is refined as needed. In the outer loop, the abstraction itself is refined by adding new predicates.

The prototype verification tool is written in Common Lisp. It uses Binary Decision Diagrams to implement the model checker and to represent the abstract system. Satisfibility checks of logic formulas over the concrete domain are carried out with CVC.

In addition to a lot of standard mutual exclusion algorithms, this method has been applied with varying degrees of automation to the following problems:

• On-The-Fly Garbage Collection Algorithm. We proved that the garbage collector is conservative, that is only unused memory is ever freed.
• FLASH Cache Coherence Protocol. We deduced an inductive invariant that was needed to do the proof in PVS.
• IBM Cache Coherence Protocol. Multiple clients contend for shared (read-only) and exclusive (read-write) access to main memory. We proved that this mutual exclusion is preserved.
• Secure Contract Signing Protocol. We proved that the protcol preserves fairness. In the context of contract signing protocols, fairness means that an individual that follows protocol steps correctly can never be cheated.
• AODV Routing Protocol. This is a routing protocol for a dynamic network where nodes can enter or leave the network at any time. We proved that routing loops can never happen in this protocol (under some assumptions).

The PredicateAbstractionExamples page has a listing of protocols that we have applied our tool to. A brief description of the syntax can be found in the MurphiSyntax page.

Publications

• [Abs] [Bib] [PS] Satyaki Das and David L. Dill. "Counter-Example Based Predicate Discovery in Predicate Abstraction", In Proceedings of FMCAD 2002, Portland, Oregon, USA, November, 2002.
• [Abs] [Bib] [PS] Satyaki Das and David L. Dill. "Successive Approximation of Abstract Transition Relations," In Proc. of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, June 2001.
• [Abs] [Bib] [PS] Satyaki Das, David L. Dill, and Seungjoon Park. "Experience with Predicate Abstraction," 11th International Conference on Computer Aided Verification, July 1999.

Software Download

Coming soon!!!