{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T16:38:02Z","timestamp":1759941482294},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_6","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T12:58:07Z","timestamp":1194872287000},"page":"89-90","source":"Crossref","is-referenced-by-count":9,"title":["Interpolants and Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"K. L.","family":"McMillan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"6_CR1","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. J. Symbolic Logic\u00a022(3), 269\u2013285 (1957)","journal-title":"J. Symbolic Logic"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R.: Rupak Majumdar, and K. L. McMillan. Abstractions from proofs. In: Principles of Prog. Lang., POPL 2004, pp. 23\u2013244 (2004)","DOI":"10.1145\/982962.964021"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","first-page":"6","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2005","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 6\u201310. Springer, Heidelberg (2005)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and sat-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"issue":"1","key":"6_CR5","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci.\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 17\u201320. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:45:11Z","timestamp":1620017111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_6","relation":{},"subject":[]}}