Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Đánh giá một bộ kiểm tra mô hình để cải tiến thuật toán và điều chỉnh hiệu suất
Tóm tắt
Bài báo này mô tả một cách tiếp cận dựa trên danh mục đầu tư cho việc kiểm tra mô hình, tức là một phương pháp trong đó nhiều động cơ kiểm tra mô hình được phối hợp để đạt được hiệu suất tốt nhất có thể trên một tập hợp thiết kế rộng và thực tế. Các thuật toán kiểm tra mô hình được đánh giá thông qua các thí nghiệm, và dữ liệu thí nghiệm truyền cảm hứng cho việc điều chỉnh gói, cũng như các tính năng và phương pháp thuật toán mới. Cách tiếp cận này, mặc dù tương tự như một số kinh nghiệm công nghiệp và học thuật, và đã được áp dụng trong các lĩnh vực khác, nhưng có vẻ như còn mới mẻ đối với lĩnh vực kiểm tra mô hình. Những đóng góp của nó nằm ở việc mô tả cách chúng tôi: (1) phân loại và phân loại các chuẩn mực một cách linh hoạt, trong suốt quá trình thực hiện thí nghiệm, (2) liên kết các vấn đề kiểm tra mô hình với các thuật toán và động cơ, (3) giới thiệu một phương pháp điều chỉnh động cho các tiểu động cơ, khai thác một phân tích hiệu suất theo thời gian thực, (4) ghi lại kết quả của các phương pháp khác nhau, và phân loại các phương pháp heuristics để nhắm tới các lớp vấn đề khác nhau. Chúng tôi cung cấp một mô tả chi tiết về các thí nghiệm được thực hiện chuẩn bị cho Cuộc thi Kiểm tra Mô hình năm 2010, nơi mà PdTRAV, công cụ xác minh học thuật của chúng tôi, đã giành chiến thắng trong hạng mục UNSAT, đồng thời xếp thứ hai trong hạng mục TỔNG THỂ.
Từ khóa
#kiểm tra mô hình #thuật toán #hiệu suất #phân tích hiệu suất #điều chỉnh thuật toánTài liệu tham khảo
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
Biere A, Klaessen KL (2010) The hardware model checking competition web page. http://fmv.jku/hwmcc10
Rice JR (1976) The algorithm selection problem. Adv Comput 15:65–118
Huberman B, Lukose R, Hogg T (1997) An economics approach to hard computational problems. Science 275(5296):51–54
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
Pulina L, Tacchella A (2009) A self-adaptive multi-engine solver for quantified boolean formulas. Constraints 14(1):80–116
Gordon M (1989) Mechanizing programming logics in higher order logic. In: Current trends in hardware verification and automated theorem proving. Springer, Berlin
Srivas M, RueßH, Cyrluk D (1997) Hardware verification using PVS. In: Formal hardware verification: methods and systems in comparison. Springer, Berlin
Kaufmann M, Manolios P, Moore JS (2000) Computer-aided reasoning: an approach. Kluwer Academic, Dordrecht
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
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
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
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
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
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
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
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
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
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
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
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
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
Biere A, Jussila T (2007) The hardware model checking competition web page. http://fmv.jku.at/hwmcc07
Berkeley Logic Interchange Format Technical report, September 1996
The AIGER format. http://fmv.jku.at/aiger/
Cabodi G, Camurati P, Quer S (2000) Symbolic forward/backward traversals of large finite state machines. Euromicro J 46(12):1137–1158
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
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
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
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
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
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
Brayton R, Mishchenko A (2010) Abc: an academic industrial-strength verification tool
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
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
Coudert O, Berthet C, Madre JC (1989) Verification of sequential machines based on symbolic execution. In: LNCS, vol 407. Springer, Berlin, pp 365–373
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
Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J Symb Log 22(3):269–285
Pudlák P (1997) Lower bounds for resolution and cutting plane proofs and monotone computations. J Symb Log 62(3):981–998
Somenzi F (2005) CUDD: CU decision diagram package—release 2.4.1. http://vlsi.colorado.edu/~fabio/CUDD/
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
Eén N, Sörensson N (2009) The Minisat SAT solver, April 2009. http://minisat.se
Mishchenko A, Chatterjee S, Brayton RK (2005) FRAIGs: a unifying representation for logic synthesis and verification. Technical report, EECS Dept, UC Berkeley, March 2005
Biere A, Jussila T (2008) The hardware model checking competition web page. http://fmv.jku.at/hwmcc08
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