Abstract
We present a new counterexample-guided abstraction refinement scheme. The scheme refines an over-approximation of the set of possible traces. Each refinement step introduces a finite automaton that recognizes a set of infeasible traces. A central idea enabling our approach is to use interpolants (assertions generated, e.g., by the infeasibility proof for an error trace) in order to automatically construct such an automaton. A data base of interpolant automata has an interesting potential for reuse of theorem proving work (from one program to another). © 2009 Springer.
Cite
CITATION STYLE
Heizmann, M., Hoenicke, J., & Podelski, A. (2009). Refinement of trace abstraction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5673 LNCS, pp. 69–85). https://doi.org/10.1007/978-3-642-03237-0_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
