Reference:

Javier Esparza, David Hansel, Peter Rossmanith, and Stefan Schwoon. Efficient algorithms for model checking pushdown systems. In E. Allen Emerson and A. Prasad Sistla, editors, Proceedings of CAV 2000, volume 1855 of Lecture Notes in Computer Science, pages 232–247. Springer, July 2000.

Abstract:

We study model checking problems for pushdown systems and linear time logics. We show that the global model checking problem (computing the set of configurations, reachable or not, that violate the formula) can be solved in time and space, where and are the size of the pushdown system and the size of a Büchi automaton for the negation of the formula. The global model checking problem for reachable configurations can be solved in time and space. In the case of pushdown systems with constant number of control states (relevant for our application), the complexity becomes time and space and time and space, respectively. We show applications of these results in the area of program analysis and present some experimental results.

Suggested BibTeX entry:

@inproceedings{EHRS00b,
    author = {Javier Esparza and David Hansel and Peter Rossmanith and Stefan Schwoon},
    booktitle = {Proceedings of CAV 2000},
    editor = {E. Allen Emerson and A. Prasad Sistla},
    month = {July},
    pages = {232--247},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Efficient Algorithms for Model Checking Pushdown Systems},
    volume = {1855},
    year = {2000}
}