Global guidance for local generalization in model checking

Springer Science and Business Media LLC
Hari Govind V K1, YuTing Chen2, Sharon Shoham3, Arie Gurfinkel1
1Department of Electrical and Computer Engineering, University of Waterloo, Waterloo, ON, Canada
2Chalmers University of Technology, Gothenburg, Sweden
3School of Computer Science, Tel-Aviv University, Tel-Aviv, Israel

Tóm tắt

AbstractSMT-based model checkers, especially IC3-style ones, are currently the most effective techniques for verification of infinite state systems. They infer global inductive invariants via local reasoning about a single step of the transition relation of a system, while employing SMT-based procedures, such as interpolation, to mitigate the limitations of local reasoning and allow for better generalization. Unfortunately, these mitigations intertwine model checking with heuristics of the underlying SMT-solver, negatively affecting stability of model checking. In this paper, we propose to tackle the limitations of locality in a systematic manner. We introduce explicit global guidance into the local reasoning performed by IC3-style algorithms. To this end, we extend the SMT-IC3 paradigm with three novel rules, designed to mitigate fundamental sources of failure that stem from locality. We instantiate these rules for Linear Integer Arithmetic and Linear Rational Aritmetic and implement them on top of Spacer solver in Z3. Our empirical results show that GSpacer, Spacer extended with global guidance, is significantly more effective than both Spacer and sole global reasoning, and, furthermore, is insensitive to interpolation.

Từ khóa


Tài liệu tham khảo

Bradley AR (2011) SAT-based model checking without unrolling. In: Verification, model checking, and abstract interpretation - 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. pp 70–87 (2011). https://doi.org/10.1007/978-3-642-18275-4_7

Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: Computer aided verification - 26th international conference, CAV 2014, held as part of the vienna summer of logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings. pp 17–34. https://doi.org/10.1007/978-3-319-08867-9_2

CHC-COMP, CHC-COMP. https://chc-comp.github.io

Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for ESC/Java. In: FME 2001: formal methods for increasing software productivity, international symposium of formal methods Europe, Berlin, Germany, March 12–16, 2001, proceedings. pp 500–517. https://doi.org/10.1007/3-540-45251-6_29

Fedyukovich G, Kaufman SJ, Bodík R (2017) Sampling invariants from frequency distributions. In: 2017 formal methods in computer aided design, FMCAD 2017, Vienna, Austria, October 2–6, 2017. pp 100–107. https://doi.org/10.23919/FMCAD.2017.8102247

Zhu H, Magill S, Jagannathan S (2018) A data-driven CHC solver. In: Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018, Philadelphia, PA, USA, June 18–22, 2018. pp 707–721. https://doi.org/10.1145/3192366.3192416

Garg P, Neider D, Madhusudan P, Roth D (2016) Learning invariants using decision trees and implication counterexamples. In: Proceedings of the 43rd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2016, St. Petersburg, FL, USA, January 20–22, 2016. pp 499–512. https://doi.org/10.1145/2837614.2837664

de Moura LM, Bjørner N (2008) Z3: An efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems, 14th international conference, TACAS 2008, held as part of the joint european conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. pp 337–340. https://doi.org/10.1007/978-3-540-78800-3_24

Krishnan HGV, Chen Y, Shoham S, Gurfinkel A (2020) Global guidance for local generalization in model checking. In: Lahiri SK, Wang C (eds) Computer aided verification - 32nd international conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, proceedings, part II. Lecture notes in computer science, vol 12225. Springer, pp 101–125. https://doi.org/10.1007/978-3-030-53291-8_7

Bjørner N, Janota M (2015) Playing with quantified satisfaction. In: 20th international conferences on logic for programming, artificial intelligence and reasoning - short presentations, LPAR 2015, Suva, Fiji, November 24–28, 2015. pp 15–27. http://www.easychair.org/publications/paper/252316

Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference record of the fourth ACM symposium on principles of programming languages, Los Angeles, California, USA, January 1977. pp 238–252. https://doi.org/10.1145/512950.512973

Bulychev PE, Kostylev EV, Zakharov VA (2009) Anti-unification algorithms and their applications in program analysis. In: Perspectives of systems informatics, 7th international andrei ershov memorial conference, PSI 2009, Novosibirsk, Russia, June 15–19, 2009. Revised papers. pp 413–423. https://doi.org/10.1007/978-3-642-11486-1_35

Yernaux G, Vanhoof W (2019) Anti-unification in constraint logic programming. TPLP 19(5–6):773–789. https://doi.org/10.1017/S1471068419000188

Benoy F, King A, Mesnard F (2005) Computing convex hulls with a linear solver. TPLP 5(1–2):259–271. https://doi.org/10.1017/S1471068404002261

The Sage Developers (2017) SageMath, the Sage mathematics software system (Version 8.1.0). https://www.sagemath.org

SV-COMP: SV-COMP. https://sv-comp.sosy-lab.org/

Leroux J, Rümmer P, Subotic P (2016) Guiding Craig interpolation with domain-specific abstractions. Acta Inf 53(4):387–424. https://doi.org/10.1007/s00236-015-0236-z

Albarghouthi A, McMillan KL (2013) Beautiful interpolants. In: Computer aided verification - 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings. pp 313–329. https://doi.org/10.1007/978-3-642-39799-8_22

Blicha M, Hyvärinen AEJ, Kofron J, Sharygina N (2019) Decomposing farkas interpolants. In: Tools and algorithms for the construction and analysis of systems - 25th international conference, TACAS 2019, held as part of the European joint conferences on theory and practice of software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, proceedings, part I. pp 3–20. https://doi.org/10.1007/978-3-030-17462-0_1

Schindler T, Jovanovic D (2018) Selfless interpolation for infinite-state model checking. In: Verification, model checking, and abstract interpretation - 19th international conference, VMCAI 2018, Los Angeles, CA, USA, January 7–9, 2018, proceedings. pp 495–515. https://doi.org/10.1007/978-3-319-73721-8_23

Champion A, Chiba T, Kobayashi N, Sato R (2018) ICE-based refinement type discovery for higher-order functional programs. In: Tools and algorithms for the construction and analysis of systems - 24th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018, proceedings, part I. pp 365–384. https://doi.org/10.1007/978-3-319-89960-2_20

McMillan KL, Kuehlmann A, Sagiv M (2009) Generalizing DPLL to richer logics. In: Computer aided verification, 21st international conference, CAV 2009, Grenoble, France, June 26–July 2, 2009. Proceedings. pp 462–476. https://doi.org/10.1007/978-3-642-02658-4_35

McMillan KL (2003) Interpolation and SAT-based model checking. In: Computer aided verification, 15th international conference, CAV 2003, Boulder, CO, USA, July 8–12, 2003, proceedings. pp 1–13. https://doi.org/10.1007/978-3-540-45069-6_1

McMillan KL (2006) Lazy abstraction with interpolants. In: computer aided verification, 18th international conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006, proceedings. pp 123–136. https://doi.org/10.1007/11817963_14

Jovanovic D, Dutertre B (2016) Property-directed k-induction. In: 2016 formal methods in computer-aided design, FMCAD 2016, Mountain View, CA, USA, October 3–6, 2016. pp 85–92. https://doi.org/10.1109/FMCAD.2016.7886665

Cimatti A, Griggio A, Mover S, Tonetta S (2016) Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods Syst Des 49(3):190–218. https://doi.org/10.1007/s10703-016-0257-4

Welp T, Kuehlmann A (2013) QF_BV model checking with property directed reachability. In: Design, automation and test in Europe, DATE 13, Grenoble, France, March 18–22, 2013. pp 791–796. https://doi.org/10.7873/DATE.2013.168

Bjørner N, Gurfinkel A (2015) Property directed polyhedral abstraction. In: Verification, model checking, and abstract interpretation - 16th international conference, VMCAI 2015, Mumbai, India, January 12–14, 2015. Proceedings. pp 263–281. https://doi.org/10.1007/978-3-662-46081-8_15

Birgmeier J, Bradley AR, Weissenbacher G (2014) Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Computer aided verification - 26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings. pp 831–848. https://doi.org/10.1007/978-3-319-08867-9_55

K HGV, Fedyukovich G, Gurfinkel A (2020) Word level property directed reachability. In: Proceedings of the 39th international conference on computer-aided design. ICCAD ’20. Association for computing machinery, New York, NY, USA. https://doi.org/10.1145/3400302.3415708

Thông tin
Thông tin xuất bản

Springer Science and Business Media LLC

Thông tin tác giả