Accession Number:

ADA461006

Title:

Predicate Abstraction of ANSI-C Programs using SAT

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Report Date:

2003-09-23

Pagination or Media Count:

26.0

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE