Predicate Abstraction with Minimum Predicates
• SEI Report
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.
Cite This SEI Report
Chaki, S., & Clarke, E. (2004, October 1). Predicate Abstraction with Minimum Predicates. Retrieved August 16, 2026, from https://www.sei.cmu.edu/library/predicate-abstraction-with-minimum-predicates/.
@techreport{chaki_2004,
author={Chaki, Sagar and Clarke, Edmund},
title={Predicate Abstraction with Minimum Predicates},
month={Oct},
year={2004},
institution={Software Engineering Institute, Carnegie Mellon University},
url={https://www.sei.cmu.edu/library/predicate-abstraction-with-minimum-predicates/},
note={Accessed: 2026-Aug-16}
}
Chaki, Sagar, and Edmund Clarke. "Predicate Abstraction with Minimum Predicates." Software Engineering Institute, Carnegie Mellon University. Software Engineering Institute, October 1, 2004. https://www.sei.cmu.edu/library/predicate-abstraction-with-minimum-predicates/.
S. Chaki, and E. Clarke, "Predicate Abstraction with Minimum Predicates," Software Engineering Institute, Carnegie Mellon University. Software Engineering Institute, 1-Oct-2004 [Online]. Available: https://www.sei.cmu.edu/library/predicate-abstraction-with-minimum-predicates/. [Accessed: 16-Aug-2026].
Chaki, Sagar, and Edmund Clarke. "Predicate Abstraction with Minimum Predicates." Software Engineering Institute, Carnegie Mellon University, Software Engineering Institute, 1 Oct. 2004. https://www.sei.cmu.edu/library/predicate-abstraction-with-minimum-predicates/. Accessed 16 Aug. 2026.
Chaki, Sagar; & Clarke, Edmund. Predicate Abstraction with Minimum Predicates. Software Engineering Institute. 2004. https://www.sei.cmu.edu/library/predicate-abstraction-with-minimum-predicates/