@inbook{0412618f3b2e4e1c92f20e7bd76cbefe,
title = "Predicate abstraction with minimum predicates",
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.",
author = "Sagar Chaki and Edmund Clarke and Alex Groce and Ofer Strichman",
year = "2003",
doi = "10.1007/978-3-540-39724-3_5",
language = "English (US)",
isbn = "354020363X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "19--34",
editor = "Daniel Geist and Enrico Tronci",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}