SAT-Based Predicate Abstraction of Programs
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. with the use of a SAT solver. The report demonstrated that SAT-based predicate abstraction outperforms the approaches that use theorem provers, since enumeration on a single SAT instance can substitute for a potentially exponential number of theorem prover calls. The advantages are particularly pronounced when the number of abstract transitions is significantly smaller than the number of possibilities that need to be checked. Furthermore, since modern SAT solvers allow for the evaluation of a large number of possible assignments to the abstract program variables, the application of a SAT engine results in a more precise transition relation of the abstract program compared to the abstraction produced by using theorem provers. This approach also simplifies (if not enables) the application of model checking to the verification of large-scale programs by eliminating analysis and refinement of redundant counterexamples.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 2005
- Accession Number
- ADA441311
Entities
People
- Daniel Kroening
- Edmund M. Clarke
- Karen Yorav
- Natasha Sharygina
Organizations
- Carnegie Mellon University