icon-carat-right menu search cmu-wordmark

Predicate Abstraction with Minimum Predicates

White Paper
Experiments show that predicate minimization can significantly reduce verification time and memory usage compared to earlier methods.
Publisher

Software Engineering Institute

Abstract

Predicate abstraction is a popular abstraction technique employed in formal software verification. A crucial requirement to make predicate abstraction effective is to use as few predicates as possible since the abstraction process is in the worst cast exponential (in both time and memory requirements) in the number of predicates involved. If a property can be proven to hold or not hold based on a given finite set of predicates P, the procedure we propose in this paper finds automatically a minimal subset of P that is sufficient for the proof. We explain how our technique can be used for more efficient verification of C programs. Our experiments show that predicate minimization can result in a significant reduction of both verification time and memory usage compared to earlier methods.