{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:17:08Z","timestamp":1759637828234},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_30","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T19:39:50Z","timestamp":1265917190000},"page":"324-336","source":"Crossref","is-referenced-by-count":78,"title":["A BDD-Based Model Checker for Recursive Programs"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"30_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, LNCS 1885, pages 113\u2013130, 2000."},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. Technical report, 2001.","DOI":"10.1007\/3-540-45139-0_7"},{"key":"30_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"Proceedings of CONCUR\u2019 97","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of CONCUR\u2019 97, LNCS 1243, pages 135\u2013150, 1997."},{"key":"30_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of CAV\u2019 00","author":"J. Esparza","year":"2000","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Proceedings of CAV\u2019 00, LNCS 1855, 2000."},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"J. Esparza and S. Schwoon. A BDD-based Model Checker for Recursive Programs. Technical report, Institut f\u00fcr Informatik, Technische Universit\u00f6t M\u00fcnchen, 2001. Available at http:\/\/www7.in.tum.de\/gruppen\/theorie\/publications\/ .","DOI":"10.1007\/3-540-44585-4_30"},{"key":"30_CR6","unstructured":"T. Jensen, D. L M\u00e9etayer, and T. Thorn. Verification of control flow based security properties. In Proceedings of 1999 IEEE Symposium on Security and Privacy, IEEE Press, 1999."},{"issue":"4","key":"30_CR7","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"J.R. Burch, E.M. Clarke, D.E. Long, K.L. MacMillan, and D.L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401\u2013424, 1994.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"30_CR8","volume-title":"Technical report","author":"F. Somenzi","year":"1998","unstructured":"F. Somenzi. Colorado University Decision Diagram Package. Technical report, University of Colorado, Boulder, 1998."},{"issue":"2","key":"30_CR9","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"Robert Tarjan","year":"1972","unstructured":"R. E. Tarjan. Depth first search and linear graph algorithms. In SICOMP 1, pages 146\u2013160, 1972.","journal-title":"SIAM Journal on Computing"},{"key":"30_CR10","unstructured":"A. Xie and P. A. Beerel. Implicit enumeration of strongly connected components. In Proceedings of ICCAD, pages 37\u201340, San Jose, CA, 1999"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T22:28:48Z","timestamp":1558823328000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}