From invariant checking to invariant inference using randomized search. (English) Zbl 1358.68197

Summary: We describe a general framework c2i for generating an invariant inference procedure from an invariant checking procedure. Given a checker and a language of possible invariants, ci generates an inference procedure that iteratively invokes two phases. The search phase uses randomized search to discover candidate invariants and the validate phase uses the checker to either prove or refute that the candidate is an actual invariant. To demonstrate the applicability of c2i, we use it to generate inference procedures that prove safety properties of numerical programs, prove non-termination of numerical programs, prove functional specifications of array manipulating programs, prove safety properties of string manipulating programs, and prove functional specifications of heap manipulating programs that use linked list data structures.


68Q60 Specification and verification (program logics, model checking, etc.)
68P05 Data structures
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI Link


[1] 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
[2] Amato, G; Parton, M; Scozzari, F, Discovering invariants via simple component analysis, J Symb Comput, 47, 1533-1560, (2012) · Zbl 1246.65077
[3] Andrieu, C; Freitas, N; Doucet, A; Jordan, MI, An introduction to MCMC for machine learning, Mach Learn, 50, 5-43, (2003) · Zbl 1033.68081
[4] Beyer D Competition on Software Verification (SV-COMP) benchmarks. https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp13/loops/
[5] Beyer, D; Henzinger, TA; Jhala, R; Majumdar, R, No article title, The software model checker blast. STTT, 9, 505-525, (2007)
[6] Beyer D, Henzinger TA, Majumdar R, Rybalchenko A (2007) Invariant synthesis for combined theories. In: VMCAI · Zbl 1132.68333
[7] Bjørner N, McMillan KL, Rybalchenko A (2013) On solving universally quantified horn clauses. In: SAS
[8] Burckhardt S, Kothari P, Musuvathi M, Nagarakatte S (2010) A randomized scheduler with probabilistic guarantees of finding bugs. In: ASPLOS
[9] Burnim J, Jalbert N, Stergiou C, Sen K (2009) Looper: Lightweight detection of infinite loops at runtime. In: ASE · Zbl 1161.68390
[10] Calcagno C, Distefano D, O’Hearn PW, Yang H (2009) Compositional shape analysis by means of bi-abduction. In: POPL · Zbl 1315.68085
[11] Chib, S; Greenberg, E, Understanding the metropolis-Hastings algorithm, Am Stat, 49, 327-335, (1995)
[12] Clarisó R, Cortadella J (2004) The octahedron abstract domain. In: SAS · Zbl 1104.68410
[13] Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: TACAS · Zbl 1031.68545
[14] Colón M, Sankaranarayanan S, Sipma H (2003) Linear invariant generation using non-linear constraint solving. In: CAV · Zbl 1278.68164
[15] Costantini G, Ferrara P, Cortesi A (2011) Static analysis of string values. In: ICFEM
[16] Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL · Zbl 1149.68389
[17] Dillig I, Dillig T, Aiken A (2010) Fluid updates: beyond strong vs. weak updates. In: ESOP · Zbl 1260.68092
[18] Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: OOPSLA · Zbl 1381.68057
[19] Ernst, MD; Perkins, JH; Guo, PJ; McCamant, S; Pacheco, C; Tschantz, MS; Xiao, C, The daikon system for dynamic detection of likely invariants, Sci Comput Prog, 69, 35-45, (2007) · Zbl 1161.68390
[20] Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for ESC/Java. In: FME
[21] Garg P, Löding C, Madhusudan P, Neider D (2013) Learning universally quantified invariants of linear data structures. In: CAV · Zbl 1322.68121
[22] Garg P, Löding C, Madhusudan P, Neider D (2014) ICE: a robust learning framework for synthesizing invariants. In: CAV · Zbl 1246.65077
[23] Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI · Zbl 1033.68081
[24] Gulavani BS, Henzinger TA, Kannan Y, Nori AV, Rajamani SK (2006) Synergy: a new algorithm for property checking. In: FSE
[25] Gulwani S, Jojic N (2007) Program verification as probabilistic inference. In: POPL · Zbl 1295.68084
[26] Gulwani S, Necula GC (2003) Discovering affine equalities using random interpretation. In: POPL · Zbl 1321.68490
[27] Gulwani S, Srivastava S, Venkatesan R (2008) Program analysis as constraint solving. In: PLDI
[28] Gulwani S, Srivastava S, Venkatesan R (2009) Constraint-based invariant inference over predicate abstraction. In: VMCAI · Zbl 1206.68087
[29] Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu RG (2008) Proving non-termination. In: POPL · Zbl 1295.68158
[30] Gupta A, Majumdar R, Rybalchenko A (2009) From tests to proofs. In: TACAS
[31] Harder M, Mellen J, Ernst MD (2003) Improving test suites via operational abstraction. In: ICSE
[32] Hoder K, Bjørner N (2012) Generalized property directed reachability. In: SAT · Zbl 1273.68229
[33] Itzhaky S, Banerjee A, Immerman N, Nanevski A, Sagiv M (2013) Effectively-propositional reasoning about reachability in linked data structures. In: CAV · Zbl 1284.68403
[34] Itzhaky S, Bjørner N, Reps TW, Sagiv M, Thakur AV (2014) Property-directed shape analysis. In: CAV · Zbl 1105.68069
[35] Ivancic F, Sankaranarayanan S NECLA static analysis benchmarks. http://www.nec-labs.com/research/system/systems_SAV-website/small_static_bench-v1.1.tar.gz
[36] Jhala R, McMillan KL (2006) A practical and complete approach to predicate refinement. In: TACAS. Springer, Berlin · Zbl 1180.68118
[37] Jung Y, Kong S, Wang BY, Yi K (2010) Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. In: VMCAI. Springer, Berlin · Zbl 1248.68272
[38] Kannan Y, Sen K (2008) Universal symbolic execution and its application to likely data structure invariant generation. In: Proceedings of the ISSTA
[39] Kong S, Jung Y, David C, Wang BY, Yi K (2010) Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: APLAS
[40] McMillan K, Rybalchenko A (2013) Combinatorial approach to some sparse-matrix problems. Technical report, Microsoft Research
[41] Miné, A, The octagon abstract domain, High-order Symb Comput, 19, 31-100, (2006) · Zbl 1105.68069
[42] de Moura LM, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS
[43] Naik M, Yang H, Castelnuovo G, Sagiv M (2012) Abstractions from tests. In: POPL · Zbl 1246.65077
[44] Neuwald, AF; Liu, JS; Lipman, DJ; Lawrence, CE, Extracting protein alignment models from the sequence database, Nucleic Acids Res, 25, 1665-1677, (1997)
[45] Nguyen T, Kapur D, Weimer W, Forrest S (2012) Using dynamic analysis to discover polynomial and array invariants. In: ICSE
[46] Nori AV, Sharma R (2013) Termination proofs from tests. In: ESEC/SIGSOFT FSE
[47] Qiu X, Garg P, Stefanescu A, Madhusudan P (2013) Natural proofs for structure, data, and separation. In: PLDI
[48] Reps TW, Sagiv S, Yorsh G (2004) Symbolic implementation of the best transformer. In: VMCAI · Zbl 1202.68255
[49] Sagiv, S; Reps, TW; Wilhelm, R, Parametric shape analysis via 3-valued logic, ACM Trans Program Lang Syst, 24, 217-298, (2002)
[50] Sankaranarayanan S, Chang RM, Jiang G, Ivancic F (2007) State space exploration using feedback constraint generation and monte-carlo sampling. In: ESEC/SIGSOFT FSE
[51] Schkufza E, Sharma R, Aiken A (2013) Stochastic superoptimization. In: ASPLOS
[52] Sharma R, Aiken A (2014) From invariant checking to invariant inference using randomized search. In: CAV · Zbl 1358.68197
[53] Sharma R, Gupta S, Hariharan B, Aiken A, Liang P, Nori AV (2013) A data driven approach for algebraic loop invariants. In: ESOP · Zbl 1381.68061
[54] Sharma R, Gupta S, Hariharan B, Aiken A, Nori AV (2013) Program verification as learning geometric concepts. In: SAS
[55] Sharma R, Nori A, Aiken A (2012) Interpolants as classifiers. In: CAV · Zbl 1033.68081
[56] Sharma R, Nori AV, Aiken A (2014) Bias-variance tradeoffs in program analysis. In: POPL · Zbl 1284.68202
[57] Solar-Lezama A (2009) The sketching approach to program synthesis. In: APLAS
[58] Srivastava S, Gulwani S (2009) Program verification using templates over predicate abstraction. In: PLDI · Zbl 1161.68390
[59] Srivastava S, Gulwani S, Foster JS (2009) VS3: SMT solvers for program verification. In: CAV
[60] Zheng Y, Zhang X, Ganesh V (2013) Z3-str: a Z3-based string solver for web application analysis. In: ESEC/SIGSOFT FSE
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.