{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T19:58:04Z","timestamp":1760644684841},"reference-count":13,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,11,1]],"date-time":"2003-11-01T00:00:00Z","timestamp":1067644800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3582,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[2003,11]]},"DOI":"10.1016\/s0890-5401(03)00139-1","type":"journal-article","created":{"date-parts":[[2003,7,7]],"date-time":"2003-07-07T13:48:27Z","timestamp":1057585707000},"page":"355-376","source":"Crossref","is-referenced-by-count":86,"title":["Model checking LTL with regular valuations for pushdown systems"],"prefix":"10.1016","volume":"186","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"given":"Anton\u0131\u0301n","family":"Ku\u010dera","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0890-5401(03)00139-1_BIB1","series-title":"SPIN 00: SPIN Workshop","first-page":"113","article-title":"Bebop: a symbolic model checker for boolean programs","volume":"vol. 1885","author":"Ball","year":"2000"},{"key":"10.1016\/S0890-5401(03)00139-1_BIB2","doi-asserted-by":"crossref","first-page":"217","DOI":"10.3233\/JCS-2001-9303","article-title":"Model checking security properties of control flow graphs","volume":"9","author":"Besson","year":"2001","journal-title":"J. Comput. Secur."},{"key":"10.1016\/S0890-5401(03)00139-1_BIB3","series-title":"Proceedings of CONCUR\u201997","first-page":"135","article-title":"Reachability analysis of pushdown automata: application to model checking","volume":"vol. 1243","author":"Bouajjani","year":"1997"},{"key":"10.1016\/S0890-5401(03)00139-1_BIB4","series-title":"Proc. ICALP\u201997","first-page":"419","article-title":"Model checking the full modal mu-calculus for infinite sequential processes","volume":"vol. 1256","author":"Burkart","year":"1997"},{"key":"10.1016\/S0890-5401(03)00139-1_BIB5","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, Temporal and modal logic, Handbook Theor. Comp. Sci. B, 1991","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"3","key":"10.1016\/S0890-5401(03)00139-1_BIB6","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","article-title":"Modalities for model checking: branching time logic strikes back","volume":"8","author":"Emerson","year":"1987","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/S0890-5401(03)00139-1_BIB7","series-title":"Proc. CAV\u201900","first-page":"232","article-title":"Efficient algorithms for model checking pushdown systems","volume":"1855","author":"Esparza","year":"2000"},{"key":"10.1016\/S0890-5401(03)00139-1_BIB8","series-title":"Proceedings of FoSSaCS\u201999","first-page":"14","article-title":"An automata-theoretic approach to interprocedural data-flow analysis","volume":"vol. 1578","author":"Esparza","year":"1999"},{"key":"10.1016\/S0890-5401(03)00139-1_BIB9","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Ku\u010dera, S. Schwoon, Model-checking LTL with regular valuations for pushdown systems, Technical Report EDI-INF-RR0044, Division of Informatics, University of Edinburgh, 2001","DOI":"10.1007\/3-540-45500-0_16"},{"key":"10.1016\/S0890-5401(03)00139-1_BIB10","series-title":"Proc. CAV\u201901","first-page":"324","article-title":"A BDD-based model checker for recursive programs","volume":"2102","author":"Esparza","year":"2001"},{"key":"10.1016\/S0890-5401(03)00139-1_BIB11","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(05)80426-8","article-title":"A direct symbolic approach to model checking pushdown systems","volume":"9","author":"Finkel","year":"1997","journal-title":"Electronic Notes Theor. Comput. Sci."},{"key":"10.1016\/S0890-5401(03)00139-1_BIB12","series-title":"IEEE Symposium on Security and Privacy","first-page":"89","article-title":"Verification of control flow based security properties","author":"Jensen","year":"1999"},{"key":"10.1016\/S0890-5401(03)00139-1_BIB13","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","article-title":"Automata theoretic techniques for modal logics of programs","volume":"32","author":"Vardi","year":"1986","journal-title":"J. Comput. Syst. Sci."}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103001391?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103001391?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T16:59:55Z","timestamp":1585069195000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540103001391"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,11]]},"references-count":13,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,11]]}},"alternative-id":["S0890540103001391"],"URL":"https:\/\/doi.org\/10.1016\/s0890-5401(03)00139-1","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[2003,11]]}}}