{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T15:46:17Z","timestamp":1744299977588},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540781622"},{"type":"electronic","value":"9783540781639"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78163-9_10","type":"book-chapter","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T10:30:06Z","timestamp":1204281006000},"page":"68-82","source":"Crossref","is-referenced-by-count":14,"title":["Approximation Refinement for Interpolation-Based Model Checking"],"prefix":"10.1007","author":[{"given":"Vijay","family":"D\u2019Silva","sequence":"first","affiliation":[]},{"given":"Mitra","family":"Purandare","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J. Kraj\u00edcek","year":"1997","unstructured":"Kraj\u00edcek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. Journal of Symbolic Logic\u00a062, 457\u2013486 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic\u00a062, 981\u2013998 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"10_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)"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.entcs.2006.12.021","volume":"174","author":"J. Marques-Silva","year":"2007","unstructured":"Marques-Silva, J.: Interpolant learning and reuse in SAT-based model checking. Electron. Notes Theor. Comput. Sci.\u00a0174, 31\u201343 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/11560548_33","volume-title":"Correct Hardware Design and Verification Methods","author":"J. Marques-Silva","year":"2005","unstructured":"Marques-Silva, J.: Improvements to the Implementation of Interpolant-Based Model Checking. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 367\u2013370. Springer, Heidelberg (2005)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation (2007)","DOI":"10.2168\/LMCS-3(4:1)2007"},{"key":"10_CR8","first-page":"366","volume-title":"International Conference on Computer-Aided Design (ICCAD)","author":"S.G. Govindaraju","year":"1998","unstructured":"Govindaraju, S.G., Dill, D.L.: Verification by approximate forward and backward reachability. In: International Conference on Computer-Aided Design (ICCAD), pp. 366\u2013370. ACM Press, New York (1998)"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/3-540-45657-0_38","volume-title":"Computer Aided Verification (CAV), Springer","author":"G. Cabodi","year":"2002","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Mixing forward and backward traversals in guided-prioritized BDD-based verification. In: Computer Aided Verification (CAV), Springer, pp. 471\u2013484. Springer, Heidelberg (2002)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1007\/978-3-540-30494-4_29","volume-title":"Formal Methods in Computer-Aided Design","author":"C. Stangier","year":"2004","unstructured":"Stangier, C., Sidle, T.: Invariant Checking Combining Forward and Backward Traversal. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 414\u2013429. Springer, Heidelberg (2004)"},{"key":"10_CR11","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P. Cousot","year":"1999","unstructured":"Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Automated Software Engineering\u00a06, 69\u201395 (1999)","journal-title":"Automated Software Engineering"},{"key":"10_CR12","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/978-3-540-74061-2_21","volume-title":"Symposium on Static Analysis (SAS)","author":"P. Cousot","year":"2007","unstructured":"Cousot, P., Ganty, P., Raskin, J.F.: Fixpoint-guided abstraction refinements. In: Symposium on Static Analysis (SAS), pp. 333\u2013348. Springer, Heidelberg (2007)"},{"key":"10_CR13","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/A:1026228213080","volume":"23","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Kupferman, O., Qadeer, S.: From Pre-historic to Post-modern symbolic model checking. Formal Methods in System Design\u00a023, 303\u2013327 (2003)","journal-title":"Formal Methods in System Design"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_7","volume-title":"Programs as Data Objects","author":"D. Mass\u00e9","year":"2001","unstructured":"Mass\u00e9, D.: Combining Forward and Backward Analyses of Temporal Properties. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol.\u00a02053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"key":"10_CR15","first-page":"772","volume-title":"International conference on Computer-aided design (ICCAD)","author":"G. Cabodi","year":"2006","unstructured":"Cabodi, G., et al.: Stepping forward with interpolants in unbounded model checking. In: International conference on Computer-aided design (ICCAD), pp. 772\u2013778. ACM Press, New York (2006)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","first-page":"227","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Somenzi","year":"2006","unstructured":"Somenzi, F., Li, B.: Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 227\u2013241. Springer, Heidelberg (2006)"},{"key":"10_CR17","first-page":"250","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem\u00a022, 250\u2013268 (1957)","journal-title":"A new form of the Herbrand-Gentzen theorem"},{"key":"10_CR18","first-page":"238","volume-title":"Principles of Programming Languages (POPL)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL), pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"10_CR19","first-page":"303","volume-title":"Program Flow Analysis: Theory and Applications","author":"P. Cousot","year":"1981","unstructured":"Cousot, P.: Semantic foundations of program analysis. In: Program Flow Analysis: Theory and Applications, pp. 303\u2013342. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"10_CR20","first-page":"108","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a SAT-solver. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Bradley, A., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Formal Methods in Computer-Aided Design (FMCAD), IEEE, Los Alamitos (to appear, 2007)","DOI":"10.1109\/FAMCAD.2007.15"},{"key":"10_CR22","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/54.867894","volume":"17","author":"F. Corno","year":"2000","unstructured":"Corno, F., Reorda, M.S., Squillero, G.: RT-level ITC\u201999 benchmarks and first ATPG results. IEEE Design and Test\u00a017, 44\u201353 (2000)","journal-title":"IEEE Design and Test"}],"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-78163-9_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:00:31Z","timestamp":1619521231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78163-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781622","9783540781639"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78163-9_10","relation":{},"subject":[]}}