search menu icon-carat-right cmu-wordmark

SAT-Based Predicate Abstraction of Programs

Technical Report
This note presents technical details of a SAT-based predicate abstraction technique used in ComFoRT (component formal reasoning technology).
Publisher

Software Engineering Institute

CMU/SEI Report Number
CMU/SEI-2005-TR-006
DOI (Digital Object Identifier)
10.1184/R1/6583565.v1

Abstract

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 Technical Report

Clarke, E., Kroening, D., Sharygina, N., & Yorav, K. (2005, September 1). SAT-Based Predicate Abstraction of Programs. (Technical Report CMU/SEI-2005-TR-006). Retrieved February 29, 2024, 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},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://doi.org/10.1184/R1/6583565.v1},
note={Accessed: 2024-Feb-29}
}

Clarke, Edmund, Daniel Kroening, Natasha Sharygina, and Karen Yorav. "SAT-Based Predicate Abstraction of Programs." (CMU/SEI-2005-TR-006). Carnegie Mellon University, Software Engineering Institute's Digital Library. 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," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Report CMU/SEI-2005-TR-006, 1-Sep-2005 [Online]. Available: https://doi.org/10.1184/R1/6583565.v1. [Accessed: 29-Feb-2024].

Clarke, Edmund, Daniel Kroening, Natasha Sharygina, and Karen Yorav. "SAT-Based Predicate Abstraction of Programs." (Technical Report CMU/SEI-2005-TR-006). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 1 Sep. 2005. https://doi.org/10.1184/R1/6583565.v1. Accessed 29 Feb. 2024.

Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; & Yorav, Karen. SAT-Based Predicate Abstraction of Programs. CMU/SEI-2005-TR-006. Software Engineering Institute. 2005. https://doi.org/10.1184/R1/6583565.v1