@inproceedings{e61be4428db44be9a0d5a60b076264b6,
title = "Efficient algorithms for model checking pushdown systems",
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 O(gPgP3gBgB3) time and O(gPgP2gBgB2) space, where gPgP and gBgB are the size of the pushdown system and the size of a B{\"u}chi automaton for the negation of the formula. The global model checking problem for reachable configurations can be solved in O(gPgP4gBgB3) time and O(gPgP4gBgB2) space. In the case of pushdown systems with constant number of control states (relevant for our application), the complexity becomes O(gPgPgBgB3) time and O(gPgPgBgB2) space and O(gPgP2gBgB3) time and O(gPgP2gBgB2) space, respectively. We show applications of these results in the area of program analysis and present some experimental results.",
author = "Javier Esparza and David Hansel and Peter Rossmanith and Stefan Schwoon",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2000.; 12th International Conference on Computer Aided Verification, CAV 2000 ; Conference date: 15-07-2000 Through 19-07-2000",
year = "2000",
doi = "10.1007/10722167_20",
language = "English",
isbn = "3540677704",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "232--247",
editor = "{Allen Emerson}, E. and {Prasad Sistla}, A.",
booktitle = "Computer Aided Verification - 12th International Conference, CAV 2000, Proceedings",
}