{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:40:30Z","timestamp":1750308030561,"version":"3.41.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2008,1]]},"abstract":"<jats:p>SAT--based Unbounded Model Checking based on Craig Interpolants is often able to overcome BDDs and other SAT--based techniques on large verification instances. Based on refutation proofs generated by SAT solvers, interpolants provide compact circuit representations of state sets, as they abstract away several nonrelevant details of the proofs. We propose three main contributions, aimed at controlling interpolant size and traversal depth. First of all, we introduce interpolant--based dynamic abstraction to reduce the support of computed interpolants. Subsequently, we propose new advances in interpolant compaction by redundancy removal. Finally, we introduce interpolant computation exploiting circuit quantification, instead of SAT refutation proofs. These techniques heavily rely on an effective application of the incremental SAT paradigm. The experimental results proposed in this paper are specifically oriented to prove properties, rather than disproving them, i.e., they target complete verification instead of simply hunting bugs. They show how this methodology is able to stretch the applicability of interpolant--based Model Checking to larger and deeper verification instances.<\/jats:p>","DOI":"10.1145\/1297666.1297669","type":"journal-article","created":{"date-parts":[[2008,2,28]],"date-time":"2008-02-28T14:02:33Z","timestamp":1204207353000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Boosting interpolation with dynamic localized abstraction and redundancy removal"],"prefix":"10.1145","volume":"13","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[{"name":"Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Murciano","sequence":"additional","affiliation":[{"name":"Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Nocco","sequence":"additional","affiliation":[{"name":"Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Quer","sequence":"additional","affiliation":[{"name":"Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,2,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Abdulla P. A. Bjesse P. and Een N. 2000. Symbolic reachability analysis based on SAT-solvers. In Tools and Algorithms for the Construction and Analysis of Systems M. I. S. Susanne Graf Ed. Vol. 1785. Springer-Verlag Berlin Germany 411--425.   Abdulla P. A. Bjesse P. and Een N. 2000. Symbolic reachability analysis based on SAT-solvers. In Tools and Algorithms for the Construction and Analysis of Systems M. I. S. Susanne Graf Ed. Vol. 1785. Springer-Verlag Berlin Germany 411--425.","DOI":"10.1007\/3-540-46419-0_28"},{"volume-title":"Proceedings of the Design Automation & Test in Europe Conference","author":"Berkelaar M.","key":"e_1_2_1_2_1","unstructured":"Berkelaar , M. and van Eijk, K. 2002. Efficient and effective redundancy removal for million-gate circuits . In Proceedings of the Design Automation & Test in Europe Conference . Paris, France, IEEE Computer Society, 1088--1088. Berkelaar, M. and van Eijk, K. 2002. Efficient and effective redundancy removal for million-gate circuits. In Proceedings of the Design Automation & Test in Europe Conference. Paris, France, IEEE Computer Society, 1088--1088."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.309942"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification","volume":"2102","author":"Bjesse P.","unstructured":"Bjesse , P. , Leonard , T. , and Mokkedem , A . 2001. Finding bugs in an alpha microprocessor using satisfiability solvers . In Proceedings of the International Conference on Computer Aided Verification . Paris, France, G. Berry, H. Comon, and A. Finkel, Eds. Lecture Notes in Computer Science , vol. 2102 . Springer-Verlag, 454--464. Bjesse, P., Leonard, T., and Mokkedem, A. 2001. Finding bugs in an alpha microprocessor using satisfiability solvers. In Proceedings of the International Conference on Computer Aided Verification. Paris, France, G. Berry, H. Comon, and A. Finkel, Eds. Lecture Notes in Computer Science, vol. 2102. Springer-Verlag, 454--464."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.275352"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.93"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the Formal Methods in Computer-Aided Design","volume":"2517","author":"Chauhan P.","unstructured":"Chauhan , P. , Clarke , E. , Kukula , J. , Sapra , S. , Veith , H. , and Wang , D . 2002. Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis . In Proceedings of the Formal Methods in Computer-Aided Design . Portland, OR, M. D. Aagaard and J. W. O'Leary, Eds. Lecture Notes in Computer Science , vol. 2517 . Springer, 35--51. Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., and Wang, D. 2002. Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In Proceedings of the Formal Methods in Computer-Aided Design. Portland, OR, M. D. Aagaard and J. W. O'Leary, Eds. Lecture Notes in Computer Science, vol. 2517. Springer, 35--51."},{"volume-title":"Proceedings of the International Conference on Computer-Aided Design","author":"Cho H.","key":"e_1_2_1_9_1","unstructured":"Cho , H. , Hachtel , G. , Jeong , S. W. , Plessier , B. , Schwarz , E. , and Somenzi , F . 1990. ATPG aspects of FSM verification . In Proceedings of the International Conference on Computer-Aided Design . San Jose, CA, 134--137. Cho, H., Hachtel, G., Jeong, S. W., Plessier, B., Schwarz, E., and Somenzi, F. 1990. ATPG aspects of FSM verification. In Proceedings of the International Conference on Computer-Aided Design. San Jose, CA, 134--137."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the International Federation for Information Processing Workshop on Applied Formal Methods for Correct VLSI Design.","volume":"1","author":"Coudert O.","unstructured":"Coudert , O. , Berthet , C. , and Madre , J. C . 1989. Verification of sequential machines using Boolean function vectors . In Proceedings of the International Federation for Information Processing Workshop on Applied Formal Methods for Correct VLSI Design. Vol. 1 . 111--128. Coudert, O., Berthet, C., and Madre, J. C. 1989. Verification of sequential machines using Boolean function vectors. In Proceedings of the International Federation for Information Processing Workshop on Applied Formal Methods for Correct VLSI Design. Vol. 1. 111--128."},{"volume-title":"International Workshop on Formal Methods in VLSI Design.","author":"Coudert O.","key":"e_1_2_1_11_1","unstructured":"Coudert , O. and Madre , J. C . 1991. Symbolic computation of the valid states of the sequential machine: Algorithms and discussion . In International Workshop on Formal Methods in VLSI Design. Coudert, O. and Madre, J. C. 1991. Symbolic computation of the valid states of the sequential machine: Algorithms and discussion. In International Workshop on Formal Methods in VLSI Design."},{"key":"e_1_2_1_12_1","unstructured":"E\u00e9n N. and S\u00f6rensson N. 2003a. Minisat SAT Solver. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/.  E\u00e9n N. and S\u00f6rensson N. 2003a. Minisat SAT Solver. http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/."},{"volume-title":"Proceedings of the 1st International Workshop on Bounded Model Checking (BMC)","author":"E\u00e9n N.","key":"e_1_2_1_13_1","unstructured":"E\u00e9n , N. and S\u00f6rensson , N . 2003b. Temporal induction by incremental sat solving . In Proceedings of the 1st International Workshop on Bounded Model Checking (BMC) . Boulder, CO. E\u00e9n, N. and S\u00f6rensson, N. 2003b. Temporal induction by incremental sat solving. In Proceedings of the 1st International Workshop on Bounded Model Checking (BMC). Boulder, CO."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"e_1_2_1_15_1","unstructured":"IBM. 2003. Ibm formal verification benchmark library. http:\/\/www.haifa.il.ibm.com\/projects\/verification\/rb_homepage\/benchmarks.html.  IBM. 2003. Ibm formal verification benchmark library. http:\/\/www.haifa.il.ibm.com\/projects\/verification\/rb_homepage\/benchmarks.html."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.776043"},{"volume-title":"Computer aided verification of coordinating processes","author":"Kurshan R. P.","key":"e_1_2_1_17_1","unstructured":"Kurshan , R. P. 1994. Computer aided verification of coordinating processes . Princeton University Press , Princeton, NJ . Kurshan, R. P. 1994. Computer aided verification of coordinating processes. Princeton University Press, Princeton, NJ."},{"volume-title":"1st International Workshop on Bounded Model Checking (BMC)","author":"Lin B.","key":"e_1_2_1_18_1","unstructured":"Lin , B. , Wang , C. , and Somenzi , F . 2003. A satisfiability-based approach to abstraction refinement in model checking . In 1st International Workshop on Bounded Model Checking (BMC) . Boulder, CO. Lin, B., Wang, C., and Somenzi, F. 2003. A satisfiability-based approach to abstraction refinement in model checking. In 1st International Workshop on Bounded Model Checking (BMC). Boulder, CO."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.998623"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_33"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734421"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the Computer Aided Verification","volume":"3725","author":"McMillan K. L.","unstructured":"McMillan , K. L. and Jhala , R . 2005. Interpolation and SAT-based model checking . In Proceedings of the Computer Aided Verification . Edinburgh, Scotland, UK. T. Ball and R. B. Jones, Eds. Lecture Notes in Computer Science , vol. 3725 . Springer, 39--51. McMillan, K. L. and Jhala, R. 2005. Interpolation and SAT-based model checking. In Proceedings of the Computer Aided Verification. Edinburgh, Scotland, UK. T. Ball and R. B. Jones, Eds. Lecture Notes in Computer Science, vol. 3725. Springer, 39--51."},{"key":"e_1_2_1_24_1","volume-title":"ABC: A system for sequential synthesis and verification","author":"Mishchenko A.","year":"2005","unstructured":"Mishchenko , A. 2005 . ABC: A system for sequential synthesis and verification , http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/. Mishchenko, A. 2005. ABC: A system for sequential synthesis and verification, http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1233501.1233679"},{"volume-title":"Proceedings of the International Workshop on Logic Synthesis","author":"Mishchenko A.","key":"e_1_2_1_26_1","unstructured":"Mishchenko , A. and Brayton , R. K . 2006b. Scalable logic synthesis using a simple circuit structure . In Proceedings of the International Workshop on Logic Synthesis . Lake Tahoe, CA. Mishchenko, A. and Brayton, R. K. 2006b. Scalable logic synthesis using a simple circuit structure. In Proceedings of the International Workshop on Logic Synthesis. Lake Tahoe, CA."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/646186.683237"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379019"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.733952"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1297666.1297669","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1297666.1297669","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:14:03Z","timestamp":1750259643000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1297666.1297669"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,1]]}},"alternative-id":["10.1145\/1297666.1297669"],"URL":"https:\/\/doi.org\/10.1145\/1297666.1297669","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2008,1]]},"assertion":[{"value":"2006-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-02-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}