{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:00:34Z","timestamp":1742914834797,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540401179"},{"type":"electronic","value":"9783540448297"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44829-2_7","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:01:40Z","timestamp":1183478500000},"page":"104-120","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A SAT Characterization of Boolean-Program Correctness"],"prefix":"10.1007","author":[{"given":"K.","family":"Rustan","sequence":"first","affiliation":[]},{"given":"M.","family":"Leino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"7_CR1","unstructured":"Fadi Aloul. Satire. http:\/\/www.eecs.umich.edu\/~{}\/faloul\/Tools\/satire\/, April 2002."},{"key":"7_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN 7","author":"T. Ball","year":"2000","unstructured":"Thomas Ball and Sriram K. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN 7, LNCS #1885, pp. 113\u2013130. Springer, 2000."},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-45420-9","volume-title":"SPIN 8","author":"T. Ball","year":"2001","unstructured":"Thomas Ball and Sriram K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 8, LNCS #2057, pp. 103\u2013122. Springer, 2001."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Bancilhon, David Maier, Yehoshua Sagiv, and Jeffrey D. Ullman. Magic sets and other strange ways to implement logic programs. In PODS 5, pp. 1\u201315. ACM Press, 1986.","DOI":"10.1145\/6012.15399"},{"key":"7_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"TACAS\u2019 99","author":"A. Biere","year":"1999","unstructured":"Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In TACAS\u2019 99, LNCS #1579, pp. 193\u2013207. Springer, 1999."},{"key":"7_CR6","series-title":"Lect Notes Comput Sci","first-page":"372","volume-title":"FMCAD 2000","author":"P. Bjesse","year":"2000","unstructured":"Per Bjesse and Koen Claessen. SAT-based verification without state space traversal. In FMCAD 2000, LNCS #1954, pp. 372\u2013389. Springer, 2000."},{"issue":"8","key":"7_CR7","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"7_CR8","unstructured":"Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"7_CR10","unstructured":"Viktor Kuncak and K. Rustan M. Leino. On computing the fixpoint of a set of boolean equations. Technical Report MSR-TR-2003-08, Microsoft Research, 2003."},{"key":"7_CR11","unstructured":"M. S. Manasse and C. G. Nelson. Correct compilation of control structures. Technical report, AT&T Bell Laboratories, September 1984."},{"issue":"5","key":"7_CR12","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. P. Marques-Silva","year":"1999","unstructured":"Jo\u00e3o P. Marques-Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506\u2013521, 1999.","journal-title":"IEEE Transactions on Computers"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In DAC 2001, pp. 530\u2013535. ACM, 2001.","DOI":"10.1145\/378239.379017"},{"key":"7_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-540-45099-3_2","volume-title":"SAS 2000","author":"A. Podelski","year":"2000","unstructured":"Andreas Podelski. Model checking as constraint solving. In SAS 2000, LNCS #1824, pp. 22\u201337. Springer, 2000."},{"key":"7_CR15","series-title":"Lect Notes Comput Sci","first-page":"108","volume-title":"FMCAD 2000","author":"M. Sheeran","year":"2000","unstructured":"Mary Sheeran, Satnam Singh, and Gunnar St\u00e5lmarck. Checking safety properties using induction and a SAT-solver. In FMCAD 2000, LNCS #1954, pp. 108\u2013125. Springer, 2000."},{"key":"7_CR16","unstructured":"Francis Tang and Martin Hofmann. Generation of verification conditions for Abadi and Leino\u2019s logic of objects. In FOOL 9, 2002. Electronic proceedings."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44829-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,6]],"date-time":"2023-02-06T20:16:20Z","timestamp":1675714580000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44829-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540401179","9783540448297"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-44829-2_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"15 April 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}