Advertisement

From Invariant Checking to Invariant Inference Using Randomized Search

  • Rahul Sharma
  • Alex Aiken
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

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.

Keywords

Cost Function Search Space Decision Procedure Inference Procedure Proposal Mechanism 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 679–685. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Bodík, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD (2013)Google Scholar
  3. 3.
    Amato, G., Parton, M., Scozzari, F.: Discovering invariants via simple component analysis. J. Symb. Comput. 47(12) (2012)Google Scholar
  4. 4.
    Andrieu, C., de Freitas, N., Doucet, A., Jordan, M.I.: An Introduction to MCMC for Machine Learning. Machine Learning 50(1) (2003)Google Scholar
  5. 5.
    Beyer, D.: Competition on Software Verification (SV-COMP) benchmarks, https://svn.sosy-lab.org/software/svbenchmarks/tags/svcomp13/loops/
  6. 6.
    Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast. STTT 9(5-6) (2007)Google Scholar
  7. 7.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378–394. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105–125. Springer, Heidelberg (2013)Google Scholar
  9. 9.
    Burnim, J., Jalbert, N., Stergiou, C., Sen, K.: Looper: Lightweight detection of infinite loops at runtime. In: ASE (2009)Google Scholar
  10. 10.
    Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL (2009)Google Scholar
  11. 11.
    Chib, S., Greenberg, E.: Understanding the Metropolis-Hastings Algorithm. The American Statistician 49(4) (1995)Google Scholar
  12. 12.
    Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Costantini, G., Ferrara, P., Cortesi, A.: Static analysis of string values. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 505–521. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  14. 14.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)Google Scholar
  15. 15.
    Dillig, I., Dillig, T., Aiken, A.: Fluid updates: Beyond strong vs. Weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 246–266. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  16. 16.
    Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: OOPSLA (2013)Google Scholar
  17. 17.
    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1-3) (2007)Google Scholar
  18. 18.
    Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001)Google Scholar
  19. 19.
    Garg, P., Löding, C., Madhusudan, P., Neider, D.: Learning universally quantified invariants of linear data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 813–829. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  20. 20.
    Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: A Robust Framework for Learning Invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69–86. Springer, Heidelberg (2014)Google Scholar
  21. 21.
    Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)Google Scholar
  22. 22.
    Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: a new algorithm for property checking. In: FSE (2006)Google Scholar
  23. 23.
    Gulwani, S., Jojic, N.: Program verification as probabilistic inference. In: POPL (2007)Google Scholar
  24. 24.
    Gulwani, S., Necula, G.C.: Discovering affine equalities using random interpretation. In: POPL (2003)Google Scholar
  25. 25.
    Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI (2008)Google Scholar
  26. 26.
    Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 120–135. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  27. 27.
    Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. In: POPL (2008)Google Scholar
  28. 28.
    Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 262–276. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  29. 29.
    Harder, M., Mellen, J., Ernst, M.D.: Improving test suites via operational abstraction. In: ICSE (2003)Google Scholar
  30. 30.
    Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  31. 31.
    Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 756–772. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  32. 32.
    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
  33. 33.
    Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  34. 34.
    Jung, Y., Kong, S., Wang, B.-Y., Yi, K.: Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 180–196. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  35. 35.
    Kannan, Y., Sen, K.: Universal symbolic execution and its application to likely data structure invariant generation. In: ISSTA (2008)Google Scholar
  36. 36.
    Kong, S., Jung, Y., David, C., Wang, B.-Y., Yi, K.: Automatically inferring quantified loop invariants by algorithmic learning from simple templates. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 328–343. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  37. 37.
    McMillan, K., Rybalchenko, A.: Combinatorial approach to some sparse-matrix problems. Tech. rep., Microsoft Research (2013)Google Scholar
  38. 38.
    de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  39. 39.
    Naik, M., Yang, H., Castelnuovo, G., Sagiv, M.: Abstractions from tests. In: POPL (2012)Google Scholar
  40. 40.
    Neuwald, A.F., Liu, J.S., Lipman, D.J., Lawrence, C.E.: Extracting protein alignment models from the sequence database. Nucleic Acids Research 25 (1997)Google Scholar
  41. 41.
    Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: ICSE (2012)Google Scholar
  42. 42.
    Nori, A.V., Sharma, R.: Termination proofs from tests. In: ESEC/SIGSOFT FSE (2013)Google Scholar
  43. 43.
    Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3) (2002)Google Scholar
  44. 44.
    Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. In: ASPLOS (2013)Google Scholar
  45. 45.
    Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 574–592. Springer, Heidelberg (2013)Google Scholar
  46. 46.
    Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Nori, A.V.: Program verification as learning geometric concepts. In: SAS (2013)Google Scholar
  47. 47.
    Sharma, R., Nori, A.V., Aiken, A.: Interpolants as classifiers. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 71–87. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  48. 48.
    Sharma, R., Nori, A.V., Aiken, A.: Bias-variance tradeoffs in program analysis. In: POPL (2014)Google Scholar
  49. 49.
    Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 4–13. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  50. 50.
    Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI (2009)Google Scholar
  51. 51.
    Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: a Z3-based string solver for web application analysis. In: ESEC/SIGSOFT FSE (2013)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Rahul Sharma
    • 1
  • Alex Aiken
    • 1
  1. 1.Stanford UniversityUSA

Personalised recommendations