@inbook{807c643c344a4f12b41cdbe0732fc586,
title = "Generation of all counter-examples for push-down systems",
abstract = "We present a new, on-the-fly algorithm that given a push-down model representing a sequential program with (recursive) procedure calls and an extended finite-state automaton representing (the negation of) a safety property, produces a succinct, symbolic representation of all counter-examples; i.e., traces of system behaviors that violate the property. The class of what we call minimum-recursion loop-free counter-examples can then be generated from this representation on an as-needed basis and presented to the user. Our algorithm is also applicable, without modification, to finite-state system models. Simultaneous consideration of multiple counter-examples can minimize the number of model-checking runs needed to recognize common root causes of property violations. We illustrate the use of our techniques via application to a Java-Tar utility and an FTP-server program, and discuss a prototype tool implementation which offers several abstraction techniques for easy-viewing of generated counter-examples.",
author = "Samik Basu and Diptikalyan Saha and Lin, \{Yow Jian\} and Smolka, \{Scott A.\}",
year = "2003",
doi = "10.1007/978-3-540-39979-7\_6",
language = "English",
isbn = "3540201750",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "79--94",
editor = "Hartmut Konig and Monika Heiner and Adam Wolisz",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}