SpringerLink
Log in

From invariant checking to invariant inference using randomized search

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

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, c2i 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4

Similar content being viewed by others

Notes

  1. The conference version, [52], lacks a comparison between pure random search and MCMC search. The treatment of numerical invariants also differs.

  2. http://stackoverflow.com/questions/17547132/slow-invariant-inference-with-horn-clauses-in-z3.

  3. https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/QALIA/.

References

  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 (2012) Discovering invariants via simple component analysis. J Symb Comput 47(12):1533–1560

    Article  MathSciNet  MATH  Google Scholar 

  3. Andrieu C, de Freitas N, Doucet A, Jordan MI (2003) An introduction to MCMC for machine learning. Mach Learn 50(1):5–43

    Article  MATH  Google Scholar 

  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 (2007) The software model checker blast. STTT 9(5–6):505–525

    Google Scholar 

  6. Beyer D, Henzinger TA, Majumdar R, Rybalchenko A (2007) Invariant synthesis for combined theories. In: VMCAI

  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

  10. Calcagno C, Distefano D, O’Hearn PW, Yang H (2009) Compositional shape analysis by means of bi-abduction. In: POPL

  11. Chib S, Greenberg E (1995) Understanding the Metropolis-Hastings algorithm. Am Stat 49(4):327–335

    Google Scholar 

  12. Clarisó R, Cortadella J (2004) The octahedron abstract domain. In: SAS

  13. Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: TACAS

  14. Colón M, Sankaranarayanan S, Sipma H (2003) Linear invariant generation using non-linear constraint solving. In: CAV

  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

  17. Dillig I, Dillig T, Aiken A (2010) Fluid updates: beyond strong vs. weak updates. In: ESOP

  18. Dillig I, Dillig T, Li B, McMillan KL (2013) Inductive invariant generation via abductive inference. In: OOPSLA

  19. Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, **ao C (2007) The Daikon system for dynamic detection of likely invariants. Sci Comput Prog 69(1–3):35–45

    Article  MathSciNet  MATH  Google Scholar 

  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

  22. Garg P, Löding C, Madhusudan P, Neider D (2014) ICE: a robust learning framework for synthesizing invariants. In: CAV

  23. Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI

  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

  26. Gulwani S, Necula GC (2003) Discovering affine equalities using random interpretation. In: POPL

  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

  29. Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu RG (2008) Proving non-termination. In: POPL

  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

  33. Itzhaky S, Banerjee A, Immerman N, Nanevski A, Sagiv M (2013) Effectively-propositional reasoning about reachability in linked data structures. In: CAV

  34. Itzhaky S, Bjørner N, Reps TW, Sagiv M, Thakur AV (2014) Property-directed shape analysis. In: CAV

  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

  37. Jung Y, Kong S, Wang BY, Yi K (2010) Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. In: VMCAI. Springer, Berlin

  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

    Google Scholar 

  41. Miné A (2006) The octagon abstract domain. High-order Symb Comput 19(1):31–100

    Article  MATH  Google Scholar 

  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

  44. Neuwald AF, Liu JS, Lipman DJ, Lawrence CE (1997) Extracting protein alignment models from the sequence database. Nucleic Acids Res 25:1665–1677

    Article  Google Scholar 

  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

  49. Sagiv S, Reps TW, Wilhelm R (2002) Parametric shape analysis via 3-valued logic. ACM Trans Program Lang Syst 24(3):217–298

    Article  Google Scholar 

  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

  53. Sharma R, Gupta S, Hariharan B, Aiken A, Liang P, Nori AV (2013) A data driven approach for algebraic loop invariants. In: ESOP

  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

  56. Sharma R, Nori AV, Aiken A (2014) Bias-variance tradeoffs in program analysis. In: POPL

  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

  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

Download references

Acknowledgments

This work was supported by National Science Foundation grant CCF-1160904, a Microsoft fellowship, and the Air Force Research Laboratory under agreement number FA8750-12-2-0020. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon.

Author information

Authors and Affiliations

  1. Department of Computer Science, Stanford University, Stanford, USA

    Rahul Sharma & Alex Aiken

Authors
  1. Rahul Sharma
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alex Aiken
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rahul Sharma.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Sharma, R., Aiken, A. From invariant checking to invariant inference using randomized search. Form Methods Syst Des 48, 235–256 (2016). https://doi.org/10.1007/s10703-016-0248-5

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-016-0248-5

Keywords

Search

Navigation