SAT-Based Predicate Abstraction of Programs
• SEI Report
Publisher
Software Engineering Institute
CMU/SEI Report Number
CMU/SEI-2005-TR-006DOI (Digital Object Identifier)
10.1184/R1/6583565.v1Abstract
Component Formal Reasoning Technology, ComFoRT, is a model-checking-based approach for analysis of component-based software designs. ComFoRT is designed to be used in a prediction-enabled component technology (PECT). A PECT provides a means to reliably predict the runtime qualities (e.g., performance and reliability) of assemblies of components from their certifiable properties (e.g., execution time and behavioral descriptions). ComFoRT uses an abstraction-based approach to cope with the complexity of analysis by reducing the size of the program models to be analyzed. This note presents technical details of a SAT-based predicate abstraction technique used in ComFoRT. The main advantage of the SAT-based method over conventional predicate abstraction techniques is that it does not require an exponential number of theorem prover calls for computing an abstract model. Additionally, the SAT-based approach computes a more precise and safe abstraction compared to existing predicate abstraction methods.
Cite This SEI Report
Clarke, E., Kroening, D., Sharygina, N., & Yorav, K. (2005, September 1). SAT-Based Predicate Abstraction of Programs. (SEI Report CMU/SEI-2005-TR-006). Retrieved June 18, 2026, from https://doi.org/10.1184/R1/6583565.v1.
@techreport{clarke_2005,
author={Clarke, Edmund and Kroening, Daniel and Sharygina, Natasha and Yorav, Karen},
title={SAT-Based Predicate Abstraction of Programs},
month={Sep},
year={2005},
number={{CMU/SEI-2005-TR-006},
institution={Software Engineering Institute, Carnegie Mellon University},
doi={10.1184/R1/6583565.v1},
url={https://doi.org/10.1184/R1/6583565.v1},
note={Accessed: 2026-Jun-18}
}
Clarke, Edmund, Daniel Kroening, Natasha Sharygina, and Karen Yorav. "SAT-Based Predicate Abstraction of Programs." (CMU/SEI-2005-TR-006). Software Engineering Institute, Carnegie Mellon University. Software Engineering Institute, September 1, 2005. https://doi.org/10.1184/R1/6583565.v1.
E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, "SAT-Based Predicate Abstraction of Programs," Software Engineering Institute, Carnegie Mellon University. Software Engineering Institute, SEI Report CMU/SEI-2005-TR-006, 1-Sep-2005 [Online]. Available: https://doi.org/10.1184/R1/6583565.v1. [Accessed: 18-Jun-2026].
Clarke, Edmund, Daniel Kroening, Natasha Sharygina, and Karen Yorav. "SAT-Based Predicate Abstraction of Programs." (SEI Report CMU/SEI-2005-TR-006). Software Engineering Institute, Carnegie Mellon University, Software Engineering Institute, 1 Sep. 2005. https://doi.org/10.1184/R1/6583565.v1. Accessed 18 Jun. 2026.
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; & Yorav, Karen. SAT-Based Predicate Abstraction of Programs. CMU/SEI-2005-TR-006. Software Engineering Institute. 2005. DOI: 10.1184/R1/6583565.v1. https://doi.org/10.1184/R1/6583565.v1