×

Learning inductive invariants by sampling from frequency distributions. (English) Zbl 1506.68054

Summary: Automated verification for program safety is reduced to the discovery safe inductive invariants, i.e., formulas that over-approximate the sets of reachable program states, but precise enough to prove unreachability of the error state. We present a framework, called FreqHorn, that follows the Syntax-Guided Synthesis paradigm to iteratively sample candidate invariants from a formal grammar and check them with an SMT solver. FreqHorn automatically constructs grammars based on either source code or bounded proofs. After each (un-)successful candidate, FreqHorn adjusts the grammars to ensure the candidate is not sampled again. The process continues either until the conjunction of successful candidates (called lemmas) is sufficient, or the search space is exhausted. Additionally, FreqHorn keeps a history of counterexamples-to-induction (CTI) which block learning a lemma. With some periodicity, it checks if there is a CTI which is invalidated by the currently learned lemmas and rechecks the failed lemma if needed. FreqHorn is able to check several candidates at the same time to filter them effectively using the well known Houdini algorithm.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q32 Computational learning theory
68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Albarghouthi A, Gurfinkel A, Chechik M (2012) From under-approximations to over-approximations and back. In: TACAS, volume 7214 of LNCS. Springer, Berlin, pp 157-172 · Zbl 1352.68140
[2] Alur R, Bodík R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: FMCAD. IEEE, pp 1-17
[3] Beyer D, Dangl M, Wendler P (2015) Boosting k-Induction with Continuously-Refined Invariants. In: CAV, Part I, volume 9206 of LNCS, pp 622-640
[4] Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic Model Checking without BDDs. In: TACAS, volume 1579 of LNCS. Springer, Berlin, pp 193-207
[5] Blicha M, Hyvärinen AEJ, Kofron J, Sharygina N (2019) Decomposing farkas interpolants. In: TACAS, Part I, volume 11427 of LNCS. Springer, Berlin, pp 3-20
[6] Bradley AR (2011) SAT-based model checking without unrolling. In: VMCAI, volume 6538 of LNCS. Springer, Berlin, pp 70-87 · Zbl 1317.68109
[7] Bradley AR (2012) Understanding IC3. In: SAT, volume 7317 of LNCS. Springer, Berlin, pp 1-14 · Zbl 1273.68222
[8] Bradley, AR; Manna, Z., Property-directed incremental invariant generation, Formal Asp Comput, 20, 4-5, 379-405 (2008) · Zbl 1149.68402 · doi:10.1007/s00165-008-0080-9
[9] Champion A, Kobayashi N, Sato R (2018) HoIce: an ICE-based non-linear horn clause solver. In: APLAS, volume 11275 of LNCS. Springer, Berlin, pp 146-156 · Zbl 1519.68045
[10] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: CAV, volume 1855 of LNCS. Springer, Berlin, pp 154-169 · Zbl 0974.68517
[11] Craig, W., Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, J Symb Log, 22, 269-285 (1957) · Zbl 0079.24502 · doi:10.2307/2963594
[12] de Moura LM, Bjørner N (2008) Z3: an efficient SMT Solver. In: TACAS, volume 4963 of LNCS. Springer, Berlin, pp 337-340
[13] Dietsch D, Heizmann M, Hoenicke J, Nutz A, Podelski A (2019) Ultimate TreeAutomizer. In: HCVS/PERR, volume 296 of EPTCS, pp 42-47 · Zbl 1483.68243
[14] Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: OOPSLA. ACM, London, pp 443-456 · Zbl 1381.68057
[15] Eén N, Mishchenko A, Brayton RK (2011) Efficient implementation of property directed reachability. In: FMCAD. IEEE, pp 125-134
[16] Fedyukovich G, Ahmad MBS, Bodík R (2017) Gradual synthesis for static parallelization of single-pass array-processing programs. In: PLDI. ACM, London, pp 572-585
[17] Fedyukovich G, Bodík R (2018) Accelerating syntax-guided invariant synthesis. In: TACAS, Part I, volume 10805 of LNCS. Springer, Berlin, pp 251-269
[18] Fedyukovich G, Gurfinkel A, Sharygina N (2014) Incremental verification of compiler optimizations. In: NFM, volume 8430 of LNCS. Springer, Berlin, pp 300-306
[19] Fedyukovich G, Gurfinkel A, Sharygina N (2015) Automated discovery of simulation between programs. In: LPAR, volume 9450 of LNCS. Springer, Berlin, pp 606-621 · Zbl 1471.68061
[20] Fedyukovich G, Gurfinkel A, Sharygina N (2016) Property directed equivalence via abstract simulation. In: CAV, vol 9780. Part II of LNCS. Springer, Berlin, pp 433-453 · Zbl 1411.68065
[21] Fedyukovich G, Kaufman S, Bodík R (2017) Sampling Invariants from Frequency Distributions. In: FMCAD. IEEE, pp 100-107
[22] Fedyukovich G, Prabhu S, Madhukar K, Gupta A (2018) Solving constrained horn clauses using syntax and data. In: FMCAD. IEEE, pp 170-178
[23] Fedyukovich G, Prabhu S, Madhukar K, Gupta A (2019) Quantified invariants via syntax-guided synthesis. In: CAV, Part I, volume 11561 of LNCS. Springer, Berlin, pp 259-277
[24] Fedyukovich G, Zhang Y, Gupta A (2018) Syntax-guided termination analysis. In: CAV, Part I, volume 10981 of LNCS. Springer, Berlin, pp 124-143 · Zbl 1511.68076
[25] Flanagan C, Leino KRM (2001) Houdini: an Annotation Assistant for ESC/Java. In: FME, volume 2021 of LNCS. Springer, Berlin, pp 500-517 · Zbl 0977.68671
[26] Garg P, Löding C, Madhusudan P, Neider D (2014) ICE: a robust framework for learning invariants. In: CAV, volume 8559 of LNCS. Springer, Berlin, pp 69-87
[27] Garg P, Neider D, Madhusudan P, Roth D (2016) Learning invariants using decision trees and implication counterexamples. In: POPL. ACM, London, pp 499-512
[28] Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI. ACM, London, pp 405-416
[29] Gulwani S, Jojic N (2007) Program verification as probabilistic inference. In: POPL. ACM, London, pp 277-289 · Zbl 1295.68084
[30] Heizmann M, Hoenicke J, Podelski A (2010) Nested interpolants. In: POPL. ACM, London, pp 471-482 · Zbl 1312.68059
[31] Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: POPL. ACM, London, pp 232-244 · Zbl 1325.68147
[32] Hoder K, Bjørner N (2012) Generalized property directed reachability. In: SAT, volume 7317 of LNCS. Springer, Berlin, pp 157-171 · Zbl 1273.68229
[33] Hojjat H, Konecný F, Garnier F, Iosif R, Kuncak V, Rümmer P (2012) A verification toolkit for numerical transition systems—tool paper. In: FM, volume 7436 of LNCS. Springer, Berlin, pp 247-251
[34] Höschele M, Zeller A (2016) Mining input grammars from dynamic taints. In: ASE. ACM, London, pp 720-725
[35] Höschele M, Zeller A (2017) Mining input grammars with AUTOGRAM. In: ICSE—companion volume. IEEE Computer Society, pp 31-34
[36] Inala JP, Polikarpova N, Qiu X, Lerner BS, Solar-Lezama A (2017) Synthesis of recursive ADT transformations from reusable templates. In: TACAS, Part I, volume 10205 of LNCS, pp 247-263 · Zbl 1452.68050
[37] Jovanovic D, Dutertre B (2016) Property-directed k-induction. In: FMCAD. IEEE, pp 85-92
[38] Kafle B, Gallagher JP, Morales JF (2016) Rahft: A tool for verifying Horn clauses using abstract interpretation and finite tree automata. In: CAV, Part I, volume 9779 of LNCS. Springer, Berlin, pp 261-268
[39] Karpenkov EG, Monniaux D (2016) Formula slicing: inductive invariants from preconditions. In: HVC, volume 10028 of LNCS. Springer, Berlin, pp 169-185
[40] Kincaid, Z.; Cyphert, J.; Breck, J.; Reps, TW, Non-linear reasoning for invariant synthesis, PACMPL, 2, POPL, 54:1-54:33 (2018)
[41] Komuravelli A, Gurfinkel A, Chaki S (2014) SMT-based model checking for recursive programs. In: CAV, volume 8559 of LNCS, pp 17-34 · Zbl 1358.68072
[42] Komuravelli A, Gurfinkel A, Chaki S, Clarke EM (2013) Automatic abstraction in SMT-based unbounded software model checking. In: CAV, volume 8044 of LNCS. Springer, Berlin, pp 846-862
[43] Le TC, Zheng G, Nguyen T (2019) SLING: using dynamic analysis to infer program invariants in separation logic. In: PLDI. ACM, London, pp 788-801
[44] McMillan KL (2003) Interpolation and SAT-based model checking. In: CAV, volume 2725 of LNCS. Springer, Berlin, pp 1-13 · Zbl 1278.68184
[45] McMillan KL (2006) Lazy abstraction with interpolants. In: CAV, volume 4144 of LNCS. Springer, Berlin, pp 123-136 · Zbl 1188.68196
[46] McMillan KL (2014) Lazy annotation revisited. In: CAV, volume 8559 of LNCS. Springer, Berlin, pp 243-259
[47] Mordvinov D, Fedyukovich G (2017) Synchronizing Constrained Horn Clauses. In: LPAR, volume 46 of EPiC Series in Computing. EasyChair, pp 338-355 · Zbl 1403.68243
[48] Padon O, McMillan KL, Panda A, Sagiv M, Shoham S (2016) Ivy: safety verification by interactive generalization. In: PLDI. ACM, London, pp 614-630
[49] Phothilimthana PM, Jelvis T, Shah R, Totla N, Chasins S, Bodík R (2014) Chlorophyll: synthesis-aided compiler for low-power spatial architectures. In: PLDI. ACM, London, pp 396-407
[50] Pick L, Fedyukovich G, Gupta A (2018) Exploiting synchrony and symmetry in relational verification. In: CAV, Part I, volume 10981 of LNCS. Springer, Berlin, pp 164-182 · Zbl 1511.68166
[51] Pu Y, Bodík R, Srivastava S (2011) Synthesis of first-order dynamic programming algorithms. In: OOPSLA. ACM, London, pp 83-98
[52] Sharma R, Aiken A (2014) From invariant checking to invariant inference using randomized search. In: CAV, volume 8559 of LNCS. Springer, Berlin, pp 88-105 · Zbl 1358.68197
[53] Solar-Lezama A, Tancau L, Bodík R, Seshia SA, Saraswat VA (2006) Combinatorial sketching for finite programs. In: ASPLOS. ACM, London, pp 404-415
[54] Suda M (2013) Triggered clause pushing for IC3. CoRR, arXiv:1307.4966
[55] Vazou N, Seidel EL, Jhala R, Vytiniotis D, Jones SLP (2014) Refinement types for Haskell. In: ICFP. ACM, London, pp 269-282 · Zbl 1345.68080
[56] Yang W, Fedyukovich G, Gupta A (2019) lemma synthesis for automating induction over algebraic data types. In: CP, volume 11802 of LNCS. Springer, Berlin, pp 600-617
[57] Zhu H, Magill S, Jagannathan S (2018) A data-driven CHC solver. In: PLDI. ACM, London, pp 707-721
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.