×

zbMATH — the first resource for mathematics

Benchmarking a model checker for algorithmic improvements and tuning for performance. (English) Zbl 1247.68160
Summary: This paper describes a portfolio-based approach for model checking, i.e., an approach in which several model checking engines are orchestrated to reach the best possible performance on a broad and real set of designs. Model checking algorithms are evaluated through experiments, and experimental data inspire package tuning, as well as new algorithmic features and methodologies. This approach, albeit similar to several industrial and academic experiences, and already applied in other domains, is somehow new to the model checking field. Its contributions lie in the description of how we: (1) characterize and classify benchmarks in a dynamic way, throughout experimental runs, (2) relate model checking problems to algorithms and engines, (3) introduce a dynamic tuning of sub-engines, exploiting an on-the-fly performance analysis, (4) record results of different approaches, and sort out heuristics to target different classes of problems. We provide a detailed description of the experiments performed in preparation of the Model Checking Competition 2010, where PdTRAV, our academic verification tool, won the UNSAT division, while ranking second in the OVERALL category.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
ABC; CUDD; SATzilla
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 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–464 · Zbl 0996.68578
[2] Biere A, Klaessen KL (2010) The hardware model checking competition web page. http://fmv.jku/hwmcc10
[3] Rice JR (1976) The algorithm selection problem. Adv Comput 15:65–118 · doi:10.1016/S0065-2458(08)60520-3
[4] Huberman B, Lukose R, Hogg T (1997) An economics approach to hard computational problems. Science 275(5296):51–54 · doi:10.1126/science.275.5296.51
[5] Xu L, Hutter F, Hoos HH, Leyton-Brown L (2008) Satzilla: Portfolio-based algorithm selection for sat. J Artif Intell Res 32(1):565–606 · Zbl 1182.68272
[6] Pulina L, Tacchella A (2009) A self-adaptive multi-engine solver for quantified boolean formulas. Constraints 14(1):80–116 · Zbl 1183.68589 · doi:10.1007/s10601-008-9051-2
[7] Gordon M (1989) Mechanizing programming logics in higher order logic. In: Current trends in hardware verification and automated theorem proving. Springer, Berlin
[8] Srivas M, RueßH, Cyrluk D (1997) Hardware verification using PVS. In: Formal hardware verification: methods and systems in comparison. Springer, Berlin
[9] Kaufmann M, Manolios P, Moore JS (2000) Computer-aided reasoning: an approach. Kluwer Academic, Dordrecht
[10] 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 ’98, London, UK. Springer, Berlin, pp 290–303
[11] 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–173 · Zbl 1117.68534
[12] Cabodi G, Camurati P, Quer S (1994) Detecting hard faults with combined approximate forward/backward symbolic techniques. In: Proc IEEE ISCAS’94, London, UK, May 1994, pp 25–30
[13] 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–320
[14] Sheeran M, Singh S, Stålmarck 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–125
[15] 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
[16] 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–13 · Zbl 1278.68184
[17] Cabodi G, Murciano M, Nocco S, Quer S (2006) Stepping forward with interpolants in unbounded model checking. In: Proc int’l conf on computer-aided design, San Jose, California, November 2006. ACM Press, New York, pp 772–778
[18] Cabodi G, Camurati P, Murciano M (2008) Automated abstraction by incremental refinement in interpolant-based model checking. In: Proc int’l conf on computer-aided design, San Jose, California, November 2008. ACM Press, New York, pp 129–136
[19] 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–340
[20] 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–212
[21] 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–395 · Zbl 05891336 · doi:10.1109/TCAD.2010.2041847
[22] 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–158 · Zbl 05744991 · doi:10.1109/TCAD.2008.2009147
[23] Biere A, Jussila T (2007) The hardware model checking competition web page. http://fmv.jku.at/hwmcc07
[24] Berkeley Logic Interchange Format Technical report, September 1996
[25] The AIGER format. http://fmv.jku.at/aiger/
[26] Cabodi G, Camurati P, Quer S (2000) Symbolic forward/backward traversals of large finite state machines. Euromicro J 46(12):1137–1158
[27] 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–484 · Zbl 1010.68521
[28] 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–556 · Zbl 05447460 · doi:10.1109/43.759068
[29] 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–130 · Zbl 0991.68547
[30] 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 · Zbl 1010.68521
[31] 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
[32] 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
[33] Brayton R, Mishchenko A (2010) Abc: an academic industrial-strength verification tool
[34] 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
[35] Een N, Mishchenko A, Amla N (2010) A single-instance incremental SAT formulation of proof and counterexample abstraction. In: Proc int’l workshop on logic synthesis, May 2010
[36] Coudert O, Berthet C, Madre JC (1989) Verification of sequential machines based on symbolic execution. In: LNCS, vol 407. Springer, Berlin, pp 365–373
[37] 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–439
[38] Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J Symb Log 22(3):269–285 · Zbl 0079.24502 · doi:10.2307/2963594
[39] Pudlák P (1997) Lower bounds for resolution and cutting plane proofs and monotone computations. J Symb Log 62(3):981–998 · Zbl 0945.03086 · doi:10.2307/2275583
[40] Somenzi F (2005) CUDD: CU decision diagram package–release 2.4.1. http://vlsi.colorado.edu/\(\sim\)fabio/CUDD/
[41] 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–432
[42] Eén N, Sörensson N (2009) The Minisat SAT solver, April 2009. http://minisat.se
[43] Mishchenko A, Chatterjee S, Brayton RK (2005) FRAIGs: a unifying representation for logic synthesis and verification. Technical report, EECS Dept, UC Berkeley, March 2005
[44] Biere A, Jussila T (2008) The hardware model checking competition web page. http://fmv.jku.at/hwmcc08
[45] 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–1691
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.