{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,6]],"date-time":"2026-05-06T15:51:18Z","timestamp":1778082678611,"version":"3.51.4"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,5,31]],"date-time":"2011-05-31T00:00:00Z","timestamp":1306800000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2011,10]]},"DOI":"10.1007\/s10703-011-0123-3","type":"journal-article","created":{"date-parts":[[2011,5,30]],"date-time":"2011-05-30T14:51:42Z","timestamp":1306767102000},"page":"205-227","source":"Crossref","is-referenced-by-count":24,"title":["Benchmarking a model checker for algorithmic improvements and tuning for performance"],"prefix":"10.1007","volume":"39","author":[{"given":"Gianpiero","family":"Cabodi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Nocco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Quer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,5,31]]},"reference":[{"key":"123_CR1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1007\/3-540-44585-4_44","volume-title":"Proc computer aided verification","author":"P Bjesse","year":"2001","unstructured":"Bjesse P, Leonard T, Mokkedem A (2001) Finding bugs in an alpha microprocessor using satisfiability solvers. In: Berry G, Comon H, Finkel A (eds) Proc computer aided verification, Paris, France, July 2001. LNCS, vol 2102. Springer, Berlin, pp 454\u2013464"},{"key":"123_CR2","unstructured":"Biere A, Klaessen KL (2010) The hardware model checking competition web page. http:\/\/fmv.jku\/hwmcc10"},{"key":"123_CR3","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S0065-2458(08)60520-3","volume":"15","author":"JR Rice","year":"1976","unstructured":"Rice JR (1976) The algorithm selection problem. Adv Comput 15:65\u2013118","journal-title":"Adv Comput"},{"issue":"5296","key":"123_CR4","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1126\/science.275.5296.51","volume":"275","author":"B Huberman","year":"1997","unstructured":"Huberman B, Lukose R, Hogg T (1997) An economics approach to hard computational problems. Science 275(5296):51\u201354","journal-title":"Science"},{"issue":"1","key":"123_CR5","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu L, Hutter F, Hoos HH, Leyton-Brown L (2008) Satzilla: Portfolio-based algorithm selection for sat. J Artif Intell Res 32(1):565\u2013606","journal-title":"J Artif Intell Res"},{"issue":"1","key":"123_CR6","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/s10601-008-9051-2","volume":"14","author":"L Pulina","year":"2009","unstructured":"Pulina L, Tacchella A (2009) A self-adaptive multi-engine solver for quantified boolean formulas. Constraints 14(1):80\u2013116","journal-title":"Constraints"},{"key":"123_CR7","volume-title":"Current trends in hardware verification and automated theorem proving","author":"M Gordon","year":"1989","unstructured":"Gordon M (1989) Mechanizing programming logics in higher order logic. In: Current trends in hardware verification and automated theorem proving. Springer, Berlin"},{"key":"123_CR8","volume-title":"Formal hardware verification: methods and systems in comparison","author":"M Srivas","year":"1997","unstructured":"Srivas M, Rue\u00dfH, Cyrluk D (1997) Hardware verification using PVS. In: Formal hardware verification: methods and systems in comparison. Springer, Berlin"},{"key":"123_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-4449-4","volume-title":"Computer-aided reasoning: an approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann M, Manolios P, Moore JS (2000) Computer-aided reasoning: an approach. Kluwer Academic, Dordrecht"},{"key":"123_CR10","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/3-540-49519-3_19","volume-title":"Proceedings of the second international conference on formal methods in computer-aided design. FMCAD \u201998","author":"G Kamhi","year":"1998","unstructured":"Kamhi G, Fix L, Binyamini Z (1998) Symbolic model checking visualization. In: Proceedings of the second international conference on formal methods in computer-aided design. FMCAD \u201998, London, UK. Springer, Berlin, pp 290\u2013303"},{"key":"123_CR11","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/978-3-540-30494-4_12","volume-title":"Proc formal methods in computer-aided design","author":"H Mony","year":"2004","unstructured":"Mony H, Baumgartner J, Paruthi V, Kanzelman R, Kuehlmann A (2004) Scalable automated verification via expert-system guided transformations. In: Proc formal methods in computer-aided design. Springer, Berlin, pp 159\u2013173"},{"key":"123_CR12","first-page":"25","volume-title":"Proc IEEE ISCAS\u201994","author":"G Cabodi","year":"1994","unstructured":"Cabodi G, Camurati P, Quer S (1994) Detecting hard faults with combined approximate forward\/backward symbolic techniques. In: Proc IEEE ISCAS\u201994, London, UK, May 1994, pp 25\u201330"},{"key":"123_CR13","first-page":"317","volume-title":"Proc 36th design automation conf","author":"A Biere","year":"1999","unstructured":"Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: Proc 36th design automation conf, New Orleans, Louisiana, June 1999. IEEE Computer Society, Los Alamitos, pp 317\u2013320"},{"key":"123_CR14","series-title":"LNCS","first-page":"108","volume-title":"Proc formal methods in computer-aided design","author":"M Sheeran","year":"2000","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a SAT solver. In: Hunt WA, Johnson SD (eds) Proc formal methods in computer-aided design, Austin, TX, USA, November 2000. LNCS, vol 1954. Springer, Berlin, pp 108\u2013125"},{"key":"123_CR15","series-title":"LNCS","volume-title":"Proc formal methods in computer-aided design","author":"P Bjesse","year":"2000","unstructured":"Bjesse P, Claessen K (2000) SAT-based verification without state space traversal. In: Proc formal methods in computer-aided design, Austin, TX, USA, LNCS, vol 1954. Springer, Berlin"},{"key":"123_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Proc computer aided verification","author":"KL McMillan","year":"2003","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr, Somenzi F (eds) Proc computer aided verification, Boulder, CO, USA, LNCS, vol 2725. Springer, Berlin, pp 1\u201313"},{"key":"123_CR17","first-page":"772","volume-title":"Proc int\u2019l conf on computer-aided design","author":"G Cabodi","year":"2006","unstructured":"Cabodi G, Murciano M, Nocco S, Quer S (2006) Stepping forward with interpolants in unbounded model checking. In: Proc int\u2019l conf on computer-aided design, San Jose, California, November 2006. ACM Press, New York, pp 772\u2013778"},{"key":"123_CR18","first-page":"129","volume-title":"Proc int\u2019l conf on computer-aided design","author":"G Cabodi","year":"2008","unstructured":"Cabodi G, Camurati P, Murciano M (2008) Automated abstraction by incremental refinement in interpolant-based model checking. In: Proc int\u2019l conf on computer-aided design, San Jose, California, November 2008. ACM Press, New York, pp 129\u2013136"},{"issue":"1","key":"123_CR19","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":"123_CR20","first-page":"205","volume-title":"Proc formal methods in computer-aided design","author":"G Cabodi","year":"2008","unstructured":"Cabodi G, Camurati P, Garcia L, Murciano M, Nocco S, Quer S (2008) Trading-off SAT search and variable quantifications for effective unbounded model checking. In: Proc formal methods in computer-aided design, Portland, Oregon, November 2008, pp 205\u2013212"},{"issue":"3","key":"123_CR21","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1109\/TCAD.2010.2041847","volume":"29","author":"G Cabodi","year":"2010","unstructured":"Cabodi G, Garcia LA, Murciano M, Nocco S, Quer S (2010) Partitioning interpolant-based verification for effective unbounded model checking. IEEE Trans Comput-Aided Des Integr Circuits Syst 29(3):382\u2013395","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"issue":"1","key":"123_CR22","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1109\/TCAD.2008.2009147","volume":"28","author":"G Cabodi","year":"2009","unstructured":"Cabodi G, Nocco S, Quer S (2009) Strengthening model checking techniques with inductive invariants. IEEE Trans Comput-Aided Des Integr Circuits Syst 28(1):154\u2013158","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"key":"123_CR23","unstructured":"Biere A, Jussila T (2007) The hardware model checking competition web page. http:\/\/fmv.jku.at\/hwmcc07"},{"key":"123_CR24","unstructured":"Berkeley Logic Interchange Format Technical report, September 1996"},{"key":"123_CR25","unstructured":"The AIGER format. http:\/\/fmv.jku.at\/aiger\/"},{"issue":"12","key":"123_CR26","first-page":"1137","volume":"46","author":"G Cabodi","year":"2000","unstructured":"Cabodi G, Camurati P, Quer S (2000) Symbolic forward\/backward traversals of large finite state machines. Euromicro J 46(12):1137\u20131158","journal-title":"Euromicro J"},{"key":"123_CR27","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1007\/3-540-45657-0_38","volume-title":"Proc computer aided verification","author":"G Cabodi","year":"2002","unstructured":"Cabodi G, Nocco S, Quer S (2002) Mixing forward and backward traversals in guided-prioritized BDD-based verification. In: Brinksma E, Larsen KG (eds) Proc computer aided verification, Copenhagen, Denmark, July 2002. LNCS, vol 2102. Springer, Berlin, pp 471\u2013484"},{"issue":"5","key":"123_CR28","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1109\/43.759068","volume":"18","author":"G Cabodi","year":"1999","unstructured":"Cabodi G, Camurati P, Quer S (1999) Improving the efficiency of BDD-based operators by means of partitioning. IEEE Trans Comput-Aided Des Integr Circuits Syst 18(5):545\u2013556","journal-title":"IEEE Trans Comput-Aided Des Integr Circuits Syst"},{"key":"123_CR29","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/3-540-44585-4_11","volume-title":"Proc computer aided verification","author":"G Cabodi","year":"2001","unstructured":"Cabodi G (2001) Meta-BDDs: a decomposed representation for layered symbolic manipulation of boolean functions. In: Berry G, Comon H, Finkel A (eds) Proc computer aided verification, Paris, France, July 2001. LNCS, vol 2102. Springer, Berlin, pp 118\u2013130"},{"key":"123_CR30","volume-title":"Proc design automation & test in Europe conf","author":"G Cabodi","year":"2007","unstructured":"Cabodi G, Nocco S, Quer S (2007) Boosting the role of inductive invariants in model checking. In: Proc design automation & test in Europe conf, Nice, France, April 2007. IEEE Computer Society, Los Alamitos"},{"key":"123_CR31","volume-title":"Proc design automation conference","author":"A Kuehlmann","year":"2001","unstructured":"Kuehlmann A, Ganai MK, Paruthi V (2001) Circuit-based Boolean reasoning. In: Proc design automation conference, Las Vegas, Nevada, June 2001. IEEE Computer Society, Los Alamitos"},{"key":"123_CR32","volume-title":"Proc design automation & test in Europe conf","author":"G Cabodi","year":"2005","unstructured":"Cabodi G, Crivellari M, Nocco S, Quer S (2005) Circuit based quantification: back to state set manipulation within unbounded model checking. In: Proc design automation & test in Europe conf, Munich, Germany, March 2005. IEEE Computer Society, Alamitos"},{"key":"123_CR33","doi-asserted-by":"crossref","unstructured":"Brayton R, Mishchenko A (2010) Abc: an academic industrial-strength verification tool","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"123_CR34","volume-title":"Proc formal methods in computer-aided design","author":"J Baumgartner","year":"2006","unstructured":"Baumgartner J, Mony H, Paruthi V, Kanzelman R, Janssen G (2006) Scalable sequential equivalence checking across arbitrary design transformations. In: Proc formal methods in computer-aided design"},{"key":"123_CR35","volume-title":"Proc int\u2019l workshop on logic synthesis","author":"N Een","year":"2010","unstructured":"Een N, Mishchenko A, Amla N (2010) A single-instance incremental SAT formulation of proof and counterexample abstraction. In: Proc int\u2019l workshop on logic synthesis, May 2010"},{"key":"123_CR36","first-page":"365","volume-title":"LNCS","author":"O Coudert","year":"1989","unstructured":"Coudert O, Berthet C, Madre JC (1989) Verification of sequential machines based on symbolic execution. In: LNCS, vol 407. Springer, Berlin, pp 365\u2013373"},{"key":"123_CR37","first-page":"428","volume-title":"Proc symposium on logic in computer science","author":"JR Burch","year":"1990","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1990) Symbolic model checking: 1020 states and beyond. In: Proc symposium on logic in computer science, Washington, DC, June 1990. Springer, Berlin, pp 428\u2013439"},{"issue":"3","key":"123_CR38","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"},{"issue":"3","key":"123_CR39","doi-asserted-by":"crossref","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k P (1997) Lower bounds for resolution and cutting plane proofs and monotone computations. J\u00a0Symb Log 62(3):981\u2013998","journal-title":"J\u00a0Symb Log"},{"key":"123_CR40","unstructured":"Somenzi F (2005) CUDD: CU decision diagram package\u2014release 2.4.1. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"123_CR41","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Proc computer aided verification","author":"RK Brayton","year":"1996","unstructured":"Brayton RK et al. (1996) VIS: a system for verification and synthesis. In: Alur R, Henzinger TA (eds) Proc computer aided verification. LNCS, vol 1102. Springer, Berlin, pp 428\u2013432"},{"key":"123_CR42","unstructured":"E\u00e9n N, S\u00f6rensson N (2009) The Minisat SAT solver, April 2009. http:\/\/minisat.se"},{"key":"123_CR43","unstructured":"Mishchenko A, Chatterjee S, Brayton RK (2005) FRAIGs: a unifying representation for logic synthesis and verification. Technical report, EECS Dept, UC Berkeley, March 2005"},{"key":"123_CR44","unstructured":"Biere A, Jussila T (2008) The hardware model checking competition web page. http:\/\/fmv.jku.at\/hwmcc08"},{"key":"123_CR45","first-page":"1686","volume-title":"Proc design automation & test in Europe conf","author":"G Cabodi","year":"2009","unstructured":"Cabodi G, Camurati P, Garcia L, Murciano M, Nocco S, Quer S (2009) Speeding up model checking by exploiting explicit and hidden verification constraints. In: Proc design automation & test in Europe conf, April 2009, pp 1686\u20131691"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0123-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0123-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0123-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T09:07:40Z","timestamp":1560244060000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0123-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,31]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,10]]}},"alternative-id":["123"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0123-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,5,31]]}}}