{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:46:31Z","timestamp":1725493591270},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434191"},{"type":"electronic","value":"9783540460022"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46002-0_17","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T02:29:59Z","timestamp":1193538599000},"page":"236-250","source":"Crossref","is-referenced-by-count":6,"title":["Resource-Constrained Model Checking of Recursive Programs"],"prefix":"10.1007","author":[{"given":"Samik","family":"Basu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K. Narayan","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L. Robert","family":"Pokorny","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C. R.","family":"Ramakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, K. Etessami, and M. Yannakakis. Analysis of recursive state machines. In Computer-Aided Verification (CAV 2001). Springer-Verlag, 2001.","DOI":"10.1007\/3-540-44585-4_18"},{"key":"17_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"Bebop: A symbolic model checker for boolean programs","author":"T. Ball","year":"2000","unstructured":"T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN00: SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, pages 113\u2013130, 2000."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"M. Benedikt, P. Godefroid, and T. Reps. Model checking unrestricted hierarchical state machines. In Twenty-Eighth Int. Colloq. on Automata, Languages, and Programming(ICALP 2001). Springer-Verlag, 2001.","DOI":"10.1007\/3-540-48224-5_54"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model checking. In Concurrency Theory (CONCURR 1997), 1997.","DOI":"10.1007\/3-540-63141-0_10"},{"key":"17_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Model checking the full-modal mu-calculus for infinite sequential processes","author":"O. Burkart","year":"1997","unstructured":"O. Burkart and B. Steffen. Model checking the full-modal mu-calculus for infinite sequential processes. In Proceedings of ICALP\u201997, volume 1256 of Lecture Notes in Computer Science, pages 419\u2013429, 1997."},{"issue":"1","key":"17_CR6","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/227595.227597","volume":"43","author":"W. Chen","year":"1996","unstructured":"W. Chen and D. S. Warren. Tabled evaluation with delaying for general logic programs. Journal of the ACM, 43(1):20\u201374, January 1996.","journal-title":"Journal of the ACM"},{"key":"17_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings of the Workshop on Logic of Programs Yorktown Heights","author":"E. M. Clarke","year":"1982","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52\u201371. Springer Verlag, 1981."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"17_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"On-the-fly verification of linear temporal logic","author":"J.-M. Couvreur","year":"1999","unstructured":"J.-M. Couvreur. On-the-fly verification of linear temporal logic. In Proceedings of FM\u201999, volume 1708 of Lecture Notes in Computer Science, pages 253\u2013271, 1999."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Computer-Aided Verification (CAV 2000), pages 232\u2013247. Springer-Verlag, 2000.","DOI":"10.1007\/10722167_20"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"J. Esparza and S. Schwoon. A bdd-based model checker for recursive programs. In Computer-Aided Verification (CAV 2001), pages 324\u2013336. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-44585-4_30"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In Second International Workshop on Verification of Infinite State Systems(INFINITY 1997), volume 9. Elsevier Science, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"17_CR13","unstructured":"L.R. Pokorny and C.R. Ramakrishnan. LTL model checking using tabled logic programming. In Workshop on Tabling in Parsing and Deduction, 2000. Available from http:\/\/www.cs.sunysb.edu\/~cram\/papers ."},{"key":"17_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Specification and verification of concurrent systems in Cesar","author":"J. P. Queille","year":"1982","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Berlin, 1982. Springer-Verlag."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 49\u201361, 1995.","DOI":"10.1145\/199448.199462"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"D. A. Schmidt and B. Steffen. Program analysis as model checking of abstract interpretations. In Static Analysis Symposium, pages 351\u2013380, 1998.","DOI":"10.1007\/3-540-49727-7_22"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"H. Tamaki and T. Sato. OLDT resolution with tabulation. In International Conference on Logic Programming, pages 84\u201398. MIT Press, 1986.","DOI":"10.1007\/3-540-16492-8_66"},{"issue":"2","key":"17_CR18","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. E. Tarjan","year":"1972","unstructured":"R. E. Tarjan. Depth first search and linear graph algorithms. SIAM Journal of Computing, 1(2):146\u2013160, 1972.","journal-title":"SIAM Journal of Computing"},{"key":"17_CR19","unstructured":"XSB. The XSB logic programming system. Available from http:\/\/xsb.sourceforge.net ."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46002-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T22:29:01Z","timestamp":1556922541000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46002-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434191","9783540460022"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-46002-0_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}