{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T22:41:56Z","timestamp":1750459316087},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540427360"},{"type":"electronic","value":"9783540455004"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45500-0_16","type":"book-chapter","created":{"date-parts":[[2007,10,25]],"date-time":"2007-10-25T19:37:33Z","timestamp":1193341053000},"page":"316-339","source":"Crossref","is-referenced-by-count":25,"title":["Model-Checking LTL with Regular Valuations for Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"given":"Anton\u00edn","family":"Ku\u010dera","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,10,10]]},"reference":[{"key":"16_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN 00: SPIN Workshop","author":"T. Ball","year":"2000","unstructured":"T. Ball and S.K. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 00: SPIN Workshop, volume 1885 of LNCS, pages 113\u2013130. Springer, 2000."},{"key":"16_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"Proc. CONCUR\u201997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model checking. In Proc. CONCUR\u201997, LNCS 1243, pages 135\u2013150."},{"key":"16_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Proc. ICALP\u201997","author":"O. Burkart","year":"1997","unstructured":"O. Burkart and B. Steffen. Model checking the full modal mu-calculus for infinite sequential processes. In Proc. ICALP\u201997, volume 1256 of LNCS, pages 419\u2013429. Springer, 1997."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and modal logic. Handbook of Theoretical Comp. Sci., B, 1991.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"3","key":"16_CR5","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"E.A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8(3):275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"16_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Proc. CAV\u201900","author":"J. Esparza","year":"2000","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Proc. CAV\u201900, LNCS 1855, pages 232\u2013247. Springer, 2000."},{"key":"16_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Proceedings of FoSSaCS\u201999","author":"J. Esparza","year":"1999","unstructured":"J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data-flow analysis. In Proceedings of FoSSaCS\u201999, volume 1578 of LNCS, pages 14\u201330. Springer, 1999."},{"key":"16_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Proc. CAV\u201901","author":"J. Esparza","year":"2001","unstructured":"J. Esparza and S. Schwoon. A BDD-based model checker for recursive programs. In Proc. CAV\u201901, LNCS 2102, pages 324\u2013336. Springer, 2001."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. Electronic Notes in Theoretical Computer Science, 9, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"T. Jensen, D. Le M\u2019etayer, and T. Thorn. Verification of control flow based security properties. In IEEE Symposium on Security and Privacy, pages 89\u2013103, 1999.","DOI":"10.1109\/SECPRI.1999.766902"},{"key":"16_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-60218-6_6","volume-title":"Proceedings of CONCUR\u201995","author":"B. Steffen","year":"1995","unstructured":"B. Steffen, A. Clasen, M. Klein, J. Knoop, and T. Margaria. The fixpoint-analysis machine. In Proceedings of CONCUR\u201995, volume 962 of LNCS, pages 72\u201387. Springer, 1995."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45500-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T00:54:39Z","timestamp":1556931279000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45500-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540427360","9783540455004"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-45500-0_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}