Carnegie Mellon University
Browse

Predicate Abstraction with Minimum Predicates.

Download (307.19 kB)
journal contribution
posted on 1978-01-01, 00:00 authored by Sagar Chaki, Edmund M Clarke, Alex Groce, Ofer Strichman
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 , the procedure we propose in this paper finds automatically a minimal subset of 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.

History

Publisher Statement

All Rights Reserved

Date

1978-01-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC