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
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.