Predicate abstraction with minimum predicates

Sagar Chaki, Edmund Clarke, Alex Groce, Ofer Strichman

Research output: Chapter in Book/Report/Conference proceedingChapter

34 Scopus citations

Abstract

Predicate abstraction is a popular abstraction technique employed in formal software verification. A crucial requirement to make predicate abstraction effective is to use as few predicates as possible, since the abstraction process is in the worst case exponential (in both time and memory requirements) in the number of predicates involved. If a property can be proven to hold or not hold based on a given finite set of predicates P, the procedure we propose in this paper finds automatically a minimal subset of P that is sufficient for the proof. We explain how our technique can be used for more efficient verification of C programs. Our experiments show that predicate minimization can result in a significant reduction of both verification time and memory usage compared to earlier methods.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsDaniel Geist, Enrico Tronci
PublisherSpringer-Verlag
Pages19-34
Number of pages16
ISBN (Print)354020363X
DOIs
StatePublished - 2003
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2860
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Predicate abstraction with minimum predicates'. Together they form a unique fingerprint.

Cite this