Predicate Abstraction of ANSI-C Programs using SAT

Abstract

Predicate abstraction is a major method for verification of software. However, the generation of the abstract Boolean program from the set of predicates and the original program suffers from an exponential number of theorem prover calls as well as from soundness issues. This paper presents a novel technique that uses an efficient SAT solver for generating the abstract transition relation of ANSI-C programs. The SATbased approach computes a more precise and safe abstraction compared to existing predicate abstraction techniques.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 23, 2003
Accession Number
ADA461006

Entities

People

  • Daniel Kroening
  • Edmund M. Clarke
  • Karen Yorav
  • Natasha Sharygina

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Arithmetic
  • Computations
  • Computer Programming
  • Computer Science
  • Concrete
  • Construction
  • Equations
  • Iterations
  • Language
  • Military Research
  • Programming Languages
  • Simulations
  • Transitions
  • Translations
  • Verification

Fields of Study

  • Computer science
  • Engineering
  • Geography

Readers

  • Computational Linguistics
  • Computational Modeling and Simulation
  • Mathematical Modeling and Probability Theory.