Predicate abstraction is a method of synthesizing the strongest inductive invariant of a system expressible as a Boolean combination of a given set of atomic predicates. A predicate selection method can be said to be complete for a given theory if it is guaranteed to eventually find atomic predicates sufficient to prove a given property, when such exist. Current heuristics are incomplete, and often diverge on simple examples. We present a practical method of predicate selection that is complete in the above sense. The method is based on interpolation and uses a "split prover", somewhat in the style of structure-based provers used in artificial intelligence. We show that it allows the verification of a variety of simple programs that cannot be verified by existing software model checkers. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Jhala, R., & McMillan, K. L. (2006). A practical and complete approach to predicate refinement. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3920 LNCS, pp. 459–473). https://doi.org/10.1007/11691372_33
Mendeley helps you to discover research relevant for your work.