Advertisement
Published in:
2008 | OriginalPaper | Chapter
A Complete Bounded Model Checking Algorithm for Pushdown Systems
Authors : Gérard Basler, Daniel Kroening, Georg Weissenbacher
Published in: Hardware and Software: Verification and Testing
Publisher: Springer Berlin Heidelberg
Pushdown systems (PDSs) consist of a stack and a finite state machine and are frequently used to model abstractions of software. They correspond to sequential recursive programs with finite-domain variables. This paper presents a novel algorithm for deciding reachability of particular locations of PDSs. We exploit the fact that most PDSs used in practice are
shallow
, and propose to use SAT-based Bounded Model Checking to search for counterexamples. Completeness is achieved by computing
universal summaries
of the procedures in the program.
