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 Note

SAT-Based Software Certification

  • February 2006
  • By Sagar Chaki
  • This 2006 report presents a technique that uses proofs to certify software.
  • Publisher: Software Engineering Institute
    CMU/SEI Report Number: CMU/SEI-2006-TN-004
  • Abstract

    This report formalizes a notion of witnesses as the basis of certifying the correctness of software. The first part of the report is concerned with witnesses for the satisfaction of linear temporal logic specifications by infinite state programs and shows how such witnesses may be constructed via predicate abstraction and validated by generating and proving verification conditions. In addition, the first part of this report proposes the use of theorem provers based on Boolean propositional satisfiability (SAT) and resolution proofs in validating these verification conditions. In addition to yielding extremely compact proofs, a SAT-based approach overcomes several limitations of conventional theorem provers when applied to the verification of programs written in real-life programming languages. 

    The second part of this report formalizes a notion of witnesses of simulation conformance between infinite state programs and finite state machine specifications. The report also proves that computing a minimal simulation relation between two finite state machines is an NP-hard problem. Finally, the report presents algorithms to construct simulation witnesses of minimal size by solving pseudo-Boolean constraints. The author's experiments on several nontrivial benchmarks suggest that a SAT-based approach can yield extremely compact proofs.

  • Download

Cite This Report

SEI

Chaki, Sagar. SAT-Based Software Certification. CMU/SEI-2006-TN-004. Software Engineering Institute, Carnegie Mellon University. 2006. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7851

IEEE

Chaki. Sagar, "SAT-Based Software Certification," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Note CMU/SEI-2006-TN-004, 2006. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7851

APA

Chaki, Sagar. (2006). SAT-Based Software Certification (CMU/SEI-2006-TN-004). Retrieved December 09, 2016, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7851

CHI

Sagar Chaki. SAT-Based Software Certification (CMU/SEI-2006-TN-004). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2006. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7851

MLA

Chaki, Sagar. 2006. SAT-Based Software Certification (Technical Report CMU/SEI-2006-TN-004). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7851

BibTex

@techreport{ChakiSATBasedSoftware2006,
title={SAT-Based Software Certification},
author={Sagar Chaki},
year={2006},
number={CMU/SEI-2006-TN-004},
institution={Software Engineering Institute, Carnegie Mellon University},
address={Pittsburgh, PA},
url={http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7851} }