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. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Basler, G., Kroening, D., & Weissenbacher, G. (2008). A complete bounded model checking algorithm for pushdown systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4899 LNCS, pp. 202–217). https://doi.org/10.1007/978-3-540-77966-7_17
Mendeley helps you to discover research relevant for your work.