{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,13]],"date-time":"2023-04-13T17:39:25Z","timestamp":1681407565239},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T00:00:00Z","timestamp":1427846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10703-015-0229-0","type":"journal-article","created":{"date-parts":[[2015,4,19]],"date-time":"2015-04-19T05:55:14Z","timestamp":1429422914000},"page":"135-162","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Optimization techniques for craig interpolant compaction in unbounded model checking"],"prefix":"10.1007","volume":"46","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carmelo","family":"Loiacono","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Danilo","family":"Vendraminetto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,20]]},"reference":[{"issue":"3","key":"229_CR1","doi-asserted-by":"crossref","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J Symb Log 22(3):269\u2013285","journal-title":"J Symb Log"},{"key":"229_CR2","doi-asserted-by":"crossref","first-page":"155","DOI":"10.2140\/pjm.1959.9.155","volume":"9","author":"RC Pacific Journal of Mathematics","year":"1959","unstructured":"Pacific Journal of Mathematics RC (1959) An interpolation theorem in the predicate calculus. Pac J Math 9:155\u2013164","journal-title":"Pac J Math"},{"key":"229_CR3","doi-asserted-by":"crossref","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Proceedings of the computer aided verification, vol 2725 of LNCS. Springer, Boulder, CO, USA, pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"229_CR4","first-page":"70","volume-title":"Sat-based model checking without unrolling. VMCAI","author":"AR Bradley","year":"2011","unstructured":"Bradley AR (2011) Sat-based model checking without unrolling. VMCAI. Springer, Austin, TX, pp 70\u201387"},{"key":"229_CR5","unstructured":"Biere A, Jussila T. The model checking competition web page, http:\/\/fmv.jku.at\/hwmcc"},{"key":"229_CR6","unstructured":"McMillan KL, Jhala R (2005) Interpolation and SAT-based model checking. In: T. Ball, R.B. Jones (eds) Proceeding of the computer aided verification, vol 3725 of LNCS. Springer, Edinburgh, pp 39\u201351"},{"key":"229_CR7","doi-asserted-by":"crossref","unstructured":"Marques-Silva J (2005) Improvements to the implementation of Interpolant-Based Model Checking. In: D. Borrione, W. Paul (eds) Proceedings of the correct hardware design and verification methods, vol 3725 of LNCS. Springer, Edinburgh, pp 367\u2013370","DOI":"10.1007\/11560548_33"},{"issue":"1","key":"229_CR8","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1145\/1297666.1297669","volume":"13","author":"G Cabodi","year":"2008","unstructured":"Cabodi G, Murciano M, Nocco S, Quer S (2008) Boosting interpolation with dynamic localized abstraction and redundancy removal. ACM Trans Des Autom Electron Syst 13(1):309\u2013340","journal-title":"ACM Trans Des Autom Electron Syst"},{"key":"229_CR9","doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati P, Murciano M (2008) Automated abstraction by incremental refinement in interpolant-based model checking. In: Proceedings of the internaional conference on computer-aided design. ACM Press, San Jose, CA, pp 129\u2013136","DOI":"10.1109\/ICCAD.2008.4681563"},{"key":"229_CR10","unstructured":"Li B, Somenzi F (2006) Efficient abstraction refinement in interpolation-based unbounded model checking. In: Tools and algorithms for the construction and analysis of systems. vol 3920, pp 227\u2013241"},{"key":"229_CR11","doi-asserted-by":"crossref","unstructured":"D\u2019Silva V, Purandare M, Kroening D (2008) Approximation refinement for interpolation-based model checking. In: F. Logozzo, D. Peled, L.D. Zuck (eds) Verification, model checking and abstract interpretation. Lecture notes in computer science, vol 4905, Springer, pp 68\u201382","DOI":"10.1007\/978-3-540-78163-9_10"},{"key":"229_CR12","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7:201\u2013215","journal-title":"J ACM"},{"key":"229_CR13","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D (1962) A machine procedure for theorem-proving. J ACM 5:394\u2013397","journal-title":"J ACM"},{"key":"229_CR14","doi-asserted-by":"crossref","unstructured":"Marques-Silva JP, Sakalla KA (1996) GRASP\u2014 A new search algorithm for satisfiability. In: Proceedings of the international conference on tool with artificial intelligence","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"229_CR15","unstructured":"Zhang L, Malik S (2003) Validating sat solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of the conference on design, automation and test in Europe, vol 1. DATE \u201903, IEEE Computer Society 10880, Washington, DC"},{"key":"229_CR16","first-page":"114","volume-title":"Linear-time reductions of resolution proofs","author":"O Bar-Ilan","year":"2009","unstructured":"Bar-Ilan O, Fuhrmann O, Hoory S, Shacham O, Strichman O (2009) Linear-time reductions of resolution proofs, vol 5394. Springer, Berlin, pp 114\u2013128"},{"key":"229_CR17","doi-asserted-by":"crossref","unstructured":"Rollini SF, Bruttomesso R, Sharygina N (2010) An efficient and flexible approach to resolution proof reduction. In: Haifa verification conference (HVC), Springer, Haifa","DOI":"10.1007\/978-3-642-19583-9_17"},{"key":"229_CR18","doi-asserted-by":"crossref","unstructured":"Fontaine P, Merz S, Paleo BW (2011) Compression of propositional resolution proofs via partial regularization. In: Proceedings of the automated deduction - CADE-23 - 23rd international conference on automated deduction, Wroclaw, Poland, July 31\u2013 August 5, 2011, pp 237\u2013251","DOI":"10.1007\/978-3-642-22438-6_19"},{"key":"229_CR19","unstructured":"Gupta A. (2012) Improved single pass algorithms for resolution proof reduction. In: ATVA, pp 107\u2013121"},{"key":"229_CR20","doi-asserted-by":"crossref","unstructured":"Cotton S. (2010) Two techniques for minimizing resolution proofs. In: Proceedings of the theory and applications of satisfiability testing - SAT 2010, 13th international conference, SAT 2010, Edinburgh, UK, July 11\u201314, 2010, pp 306\u2013312","DOI":"10.1007\/978-3-642-14186-7_26"},{"key":"229_CR21","doi-asserted-by":"crossref","unstructured":"Saluja N, Khatri SP (2004) A robust algorithm for approximate compatible observability don\u2019t care computation. In: Proceedings design automation conference, pp 422\u2013427","DOI":"10.1145\/996566.996688"},{"key":"229_CR22","doi-asserted-by":"crossref","unstructured":"Savoj H, Brayton RK (1990) The use of observability and external don\u2019t cares for the simplification of multi-level networks. In: Proceedings of the design automation conference, pp 297\u2013301","DOI":"10.1145\/123186.123280"},{"key":"229_CR23","doi-asserted-by":"crossref","unstructured":"Savoj H, Brayton RK, Touati HJ (1991) Extracting local don\u2019t cares for network optimization. In: ICCAD, pp 514\u2013517","DOI":"10.1109\/ICCAD.1991.185319"},{"key":"229_CR24","unstructured":"Mishchenko A, Brayton RK (2007) Sat-based complete don\u2019t-care computation for network optimization. CoRR Arxiv:0710.4695"},{"key":"229_CR25","doi-asserted-by":"crossref","unstructured":"McMillan KL (2002) Applying sat methods in unbounded symbolic model checking. In: E Brinksma, KG Larsen (eds) CAV, Lecture notes in computer science, vol 2404. Springer, pp 250\u2013264","DOI":"10.1007\/3-540-45657-0_19"},{"key":"229_CR26","unstructured":"McMillan KL, Labs CB (2005) Don\u2019t-care computation using k-clause approximation. In: International Workshop on Logic & Synthesis"},{"key":"229_CR27","doi-asserted-by":"crossref","unstructured":"Brayton RK, Mishchenko A (2010) Abc: An academic industrial-strength verification tool. In: T Touili, B Cook, P Jackson (eds) CAV, Lecture notes in computer science, vol 6174, Springer, pp 24\u201340","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"229_CR28","unstructured":"Mishchenk A (2005) ABC: A system for sequential synthesis and verification, http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"229_CR29","doi-asserted-by":"crossref","unstructured":"Cabodi G, Loiacono C, Vendraminetto D (2013) Optimization techniques for craig interpolant compaction in unbounded model checking. In: Proceedings of the design automation & test in Europe conference, IEEE Computer Society, Grenoble, France, pp 1417\u20131422","DOI":"10.7873\/DATE.2013.289"},{"key":"229_CR30","doi-asserted-by":"crossref","unstructured":"Bruttomesso R, Rollini SF, Sharygina N, Tsitovich A (2010) Flexible interpolation with local proof transformations. In: International conference of computer aided design (ICCAD), IEEE Computer Society, San Jose, USA","DOI":"10.1109\/ICCAD.2010.5654297"},{"key":"229_CR31","unstructured":"Sharygina N (2013) PeRIPLO. Formal verification at University of Lugano, http:\/\/verify.inf.unisi.ch\/periplo.html"},{"key":"229_CR32","doi-asserted-by":"crossref","unstructured":"Bloem R, Malik S, Schlaipfer M, Weissenbacher G (2014) Reduction of resolution refutations and interpolants via subsumption. In: Proceedings of the hardware and software: verification and testing - 10th international Haifa verification conference, HVC 2014, Haifa, Israel, November 18\u201320, 2014, pp 188\u2013203","DOI":"10.1007\/978-3-319-13338-6_15"},{"key":"229_CR33","unstructured":"Chockler H, Ivril A, Matsliah A (2012) Computing interpolants without proofs. In: Proceedings of the 7th international Haifa verification conference on hardware and software: verification and testing. HVC \u201912"},{"key":"229_CR34","doi-asserted-by":"crossref","unstructured":"Vizel Y, Ryvchin V, Nadel A (2013) Efficient generation of small interpolants in cnf. In: CAV, pp 330\u2013346","DOI":"10.1007\/978-3-642-39799-8_23"},{"key":"229_CR35","doi-asserted-by":"crossref","unstructured":"Vizel Y, Gurfinkel A (2014) Interpolating property directed reachability. CAV, pp 260\u2013276","DOI":"10.1007\/978-3-319-08867-9_17"},{"key":"229_CR36","doi-asserted-by":"crossref","unstructured":"Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th design automation conference, IEEE Computer Society, Las Vegas, NV","DOI":"10.1145\/378239.379017"},{"key":"229_CR37","unstructured":"E\u00e9n N, S\u00f6rensson N (2009) The minisat SAT solver, http:\/\/minisat.se"},{"key":"229_CR38","unstructured":"Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th design automation conference, IEEE Computer Society, New Orleans, LA, pp 317\u2013320"},{"key":"229_CR39","unstructured":"E\u00e9n N (May 2007) Cut sweeping. Technical report, Cadence Research Labs, Berkeley, USA"},{"key":"229_CR40","doi-asserted-by":"crossref","unstructured":"Kuehlmann A, Krohm F (1997) Equivalence checking using cuts and heaps. In: Proceedings of the 34th design automation conference, IEEE Computer Society, Anaheim, CA, pp 263\u2013268","DOI":"10.1109\/DAC.1997.597155"},{"key":"229_CR41","doi-asserted-by":"crossref","unstructured":"Kuehlmann A (2004) Dynamic transition relation simplification for bounded property checking. In: Proceedings of the international conference on computer-aided design, IEEE Computer Society, San Jose, CA, pp 50\u201357","DOI":"10.1109\/ICCAD.2004.1382542"},{"key":"229_CR42","doi-asserted-by":"crossref","unstructured":"Bjesse P, Boralv A (2004) DAG-aware circuit compression for formal verification. In: Proceedings of the international conference on computer-aided design, IEEE Computer Society, San Jose, CA","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"229_CR43","unstructured":"Brayton RK, Chatterjee S, Mishchenko A (2006) DAG-aware aig rewriting: a fresh look at combinational logic synthesis. In: Proceedings design automation conference, pp 532\u2013536"},{"key":"229_CR44","doi-asserted-by":"crossref","unstructured":"Mishchenko A, Chatterjee S, Brayton R (2006) Dag-aware aig rewriting: a fresh look at combinational logic synthesis. In: In DAC 06\u2014 Proceedings of the 43rd annual conference on design automation, ACM Press, pp 532\u2013536","DOI":"10.1145\/1146909.1147048"},{"issue":"2","key":"229_CR45","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/s10703-011-0123-3","volume":"39","author":"G Cabodi","year":"2011","unstructured":"Cabodi G, Nocco S, Quer S (2011) Benchmarking a model checker for algorithmic improvements and tuning for performance. Form Methods Syst Des 39(2):205\u2013227","journal-title":"Form Methods Syst Des"},{"key":"229_CR46","unstructured":"Formal-Methods-Group (2014) PdTrav Tool, http:\/\/fmgroup.polito.it\/index.php\/download\/viewcategory\/3-pdtrav-package"},{"key":"229_CR47","unstructured":"Biere A, Heljanko K (2014) The model checking competition web page, http:\/\/fmv.jku.at\/hwmcc14"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0229-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0229-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0229-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,23]],"date-time":"2019-08-23T19:48:37Z","timestamp":1566589717000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-015-0229-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4]]},"references-count":47,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["229"],"URL":"https:\/\/doi.org\/10.1007\/s10703-015-0229-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,4]]}}}