Predicate abstraction is a major abstraction technique for the verification of software. Data is abstracted by means of Boolean variables, which keep track of predicates over the data. In many cases, the technique suffers from the fact that it requires at least one predicate for each iteration of a loop construct in the program. We propose to extract looping counterexamples from the abstract model, and to parameterize the simulation instance in the number of loop iterations. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Kroening, D., & Weissenbacher, G. (2006). Counterexamples with loops for predicate abstraction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4144 LNCS, pp. 152–165). Springer Verlag. https://doi.org/10.1007/11817963_16
Mendeley helps you to discover research relevant for your work.