SAT-Based Predicate Abstraction of Programs
September 2005 • Technical Report
Edmund Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav (IBM)
This note presents technical details of a SAT-based predicate abstraction technique used in ComFoRT (component formal reasoning technology).
Software Engineering Institute
CMU/SEI Report Number
DOI (Digital Object Identifier):10.1184/R1/6583565.v1
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.