Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

Technical Report

SAT-Based Predicate Abstraction of Programs

  • September 2005
  • By 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).
  • Publisher: Software Engineering Institute
    CMU/SEI Report Number: CMU/SEI-2005-TR-006
  • 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.

  • Download

Cite This Report

SEI

Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; & Yorav, Karen. SAT-Based Predicate Abstraction of Programs. CMU/SEI-2005-TR-006. Software Engineering Institute, Carnegie Mellon University. 2005. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7629

IEEE

Clarke. Edmund, Kroening. Daniel, Sharygina. Natasha, and Yorav. Karen, "SAT-Based Predicate Abstraction of Programs," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Report CMU/SEI-2005-TR-006, 2005. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7629

APA

Clarke, Edmund., Kroening, Daniel., Sharygina, Natasha., & Yorav, Karen. (2005). SAT-Based Predicate Abstraction of Programs (CMU/SEI-2005-TR-006). Retrieved April 29, 2017, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7629

CHI

Edmund Clarke, Daniel Kroening, Natasha Sharygina, & Karen Yorav. SAT-Based Predicate Abstraction of Programs (CMU/SEI-2005-TR-006). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2005. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7629

MLA

Clarke, Edmund., Kroening, Daniel., Sharygina, Natasha., & Yorav, Karen. 2005. SAT-Based Predicate Abstraction of Programs (Technical Report CMU/SEI-2005-TR-006). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7629

BibTex

@techreport{ClarkeSATBasedPredicate2005,
title={SAT-Based Predicate Abstraction of Programs},
author={Edmund Clarke and Daniel Kroening and Natasha Sharygina and Karen Yorav},
year={2005},
number={CMU/SEI-2005-TR-006},
institution={Software Engineering Institute, Carnegie Mellon University},
address={Pittsburgh, PA},
url={http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7629} }