{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T19:08:29Z","timestamp":1769972909881,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631415","type":"print"},{"value":"9783540691884","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63141-0_10","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:08:26Z","timestamp":1330297706000},"page":"135-150","source":"Crossref","is-referenced-by-count":306,"title":["Reachability analysis of pushdown automata: Application to model-checking"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"10_CR1","unstructured":"A.V. Aho, J.E. Hopcroft, and J.D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1976."},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The Algorithmic Analysis of Hybrid Systems. TCS, 138, 1995.","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur and D. Dill. A Theory of Timed Automata. TCS, 126, 1994.","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"E. Asarin, O. Maler, and A. Pnueli. Symbolic Controller Synthesis for Discrete and Timed Systems. In Hybrid Systems II. LNCS 999, 1995.","DOI":"10.1007\/3-540-60472-3_1"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"B. Boigelot and P. Godefroid. Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs. In CAV'96. LNCS 1102, 1996.","DOI":"10.1007\/3-540-61474-5_53"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"R.V. Book and F. Otto. String-Rewriting Systems. Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4613-9771-7"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model Checking. Tech. Rep. Verimag, 1997. ftp:\/\/ftp.imag.fr\/imag\/SPECTRE\/ODED\/pda.ps.gz, http:\/\/papa.informatik.tu-muenchen.de\/forschung\/sfb342_a3\/refs.html.","DOI":"10.1007\/3-540-63141-0_10"},{"key":"10_CR8","unstructured":"A. Bouajjani and O. Maler. Reachability Analysis of Pushdown Automata. In Infinity'96. tech. rep. MIP-9614, Univ. Passau, 1996."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"J.C. Bradfield. Verifying Temporal Properties of Systems. Birkhauser, 1992.","DOI":"10.1007\/978-1-4684-6819-9"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"R. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, 24, 1992.","DOI":"10.1145\/136035.136043"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"O. Burkart and B. Steffen. Model Checking for Context-Free Processes. In CONCUR'92, 1992. LNCS 630.","DOI":"10.1007\/BFb0084787"},{"key":"10_CR12","unstructured":"O. Burkart and B. Steffen. Composition, Decomposition and Model-Checking of Pushdown Processes. Nordic Journal of Computing, 2, 1995."},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, and E. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications: A Practical Approach. In POPL'83. ACM, 1983.","DOI":"10.1145\/567067.567080"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Automated Temporal Reasoning about Reactive Systems. In Logics for Concurrency. LNCS 1043, 1996.","DOI":"10.1007\/3-540-60915-6_3"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A Direct Symbolic Approach to Model Checking Pushdown Systems. In Personal communication, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"10_CR16","unstructured":"G. Holzmann. Basic SPIN manual. Technical report, Bell Laboratories, 1994."},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model-Checking: an Approach to the State-Explosion Problem. Kluwer, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The Temporal Logic of Programs. In FOCS'77. IEEE, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. A Temporal Fixpoint Calculus. In POPL'88. ACM, 1988.","DOI":"10.1145\/73560.73582"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. Alternating Automata and Program Verification. In Computer Science Today. LNCS 1000, 1995.","DOI":"10.1007\/BFb0015261"},{"key":"10_CR21","unstructured":"M.Y. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. In LICS'86. IEEE, 1986."},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"I. Walukiewicz. Pushdown Processes: Games and Model Checking. In CAV'96. LNCS 1102, 1996.","DOI":"10.7146\/brics.v3i54.20057"}],"container-title":["Lecture Notes in Computer Science","CONCUR '97: Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63141-0_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:16:04Z","timestamp":1605647764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63141-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631415","9783540691884"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-63141-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}