Generation of All Counter-Examples for Push-Down Systems

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 disrototype tool implementation which offers several abstraction techniques for easy-viewing of generated counter...

• Type: Conference
• Year: 2003
• Where: FORTE
• Authors: Samik Basu, Diptikalyan Saha, Yow-Jian Lin, Scott A. Smolka
• Keywords: Extended finite-state Automaton, FORTE 2003, FORTE 2007, Minimum-recursion Loop-free Counter-examples, On-the-fly Algorithm