Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning

  • Long H. PhamEmail author
  • Jun Sun
  • Quang Loc Le
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11893)


Analyzing and verifying heap-manipulating programs automatically is challenging. A key for fighting the complexity is to develop compositional methods. For instance, many existing verifiers for heap-manipulating programs require user-provided specification for each function in the program in order to decompose the verification problem. The requirement, however, often hinders the users from applying such tools. To overcome the issue, we propose to automatically learn heap-related program invariants in a property-guided way for each function call. The invariants are learned based on the memory graphs observed during test execution and improved through memory graph mutation. We implemented a prototype of our approach and integrated it with two existing program verifiers. The experimental results show that our approach enhances existing verifiers effectively in automatically verifying complex heap-manipulating programs with multiple function calls.



This research is supported by MOE research grant MOE2016-T2-2-123.


  1. 1.
    Facebook Infer.
  2. 2.
  3. 3.
  4. 4.
    Albarghouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015, pp. 634–660 (2015). Scholar
  5. 5.
    Berdine, J., Cox, A., Ishtiaq, S., Wintersteiger, C.M.: Diagnosing abstraction failure for separation logic-based analyses. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012, pp. 155–173 (2012). Scholar
  6. 6.
    Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, pp. 184–190 (2011). Scholar
  7. 7.
    Brockschmidt, M., Chen, Y., Kohli, P., Krishna, S., Tarlow, D.: Learning shape analysis. In: Ranzato, F. (ed.) SAS 2017, pp. 66–87 (2017). Scholar
  8. 8.
    Bshouty, N.H., Goldman, S.A., Mathias, H.D., Suri, S., Tamaki, H.: Noise-tolerant distribution-free learning of general geometric concepts. J. ACM 45(5), 863–890 (1998). Scholar
  9. 9.
    Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional Shape Analysis by Means of Bi-Abduction. J. ACM 58(6), 26:1–26:66 (2011). Scholar
  10. 10.
    Chin, W., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program 77(9), 1006–1036 (2012). Scholar
  11. 11.
    Cleve, H., Zeller, A.: Locating causes of program failures. In: Roman, G., Griswold, W.G., Nuseibeh, B. (eds.) ICSE 2005, pp. 342–351 (2005).
  12. 12.
    Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: Harris, G.E. (ed.) OOPSLA 2008, pp. 213–226 (2008).
  13. 13.
    Dudka, K., Peringer, P., Vojnar, T.: Predator: a practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, pp. 372–378 (2011). Scholar
  14. 14.
    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), 35–45 (2007). Scholar
  15. 15.
    Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001, pp. 500–517 (2001). Scholar
  16. 16.
    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, pp. 813–829 (2013). Scholar
  17. 17.
    Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: a robust framework for learning invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 69–87 (2014). Scholar
  18. 18.
    Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: Bodík, R., Majumdar, R. (eds.) POPL 2016, pp. 499–512 (2016).
  19. 19.
    Ginsburg, S., Spanier, E.: Semigroups, presburger formulas, and languages. Pac. J. Math. 16(2), 285–296 (1966)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Pasareanu, C.S. (eds.) CAV 2015, pp. 343–361 (2015). Scholar
  21. 21.
    Holík, L., Hruska, M., Lengál, O., Rogalewicz, A., Simácek, J., Vojnar, T.: Forester: from heap shapes to automata predicates - (competition contribution). In: Legay, A., Margaria, T. (eds.) TACAS 2017, pp. 365–369 (2017). Scholar
  22. 22.
    Holík, L., Lengál, O., Rogalewicz, A., Simácek, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013, pp. 740–755 (2013). Scholar
  23. 23.
    Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Hankin, C., Schmidt, D. (eds.) POPL 2001, pp. 14–26 (2001)CrossRefGoogle Scholar
  24. 24.
    Itzhaky, S., Bjørner, N., Reps, T.W., Sagiv, M., Thakur, A.V.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 35–51 (2014). Scholar
  25. 25.
    Kulkarni, S., Mangal, R., Zhang, X., Naik, M.: Accelerating program analyses by cross-program training. In: Visser, E., Smaragdakis, Y. (eds.) OOPSLA 2016, pp. 359–377 (2016).
  26. 26.
    Le, Q.L., Gherghina, C., Qin, S., Chin, W.: Shape analysis via second-order bi-abduction. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 52–68 (2014). Scholar
  27. 27.
    Le, Q.L., Sun, J., Chin, W.: Satisfiability modulo heap-based programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, pp. 382–404 (2016). Scholar
  28. 28.
    Le, Q.L., Sun, J., Qin, S.: Frame inference for inductive entailment proofs in separation logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, pp. 41–60 (2018). Scholar
  29. 29.
    Le, Q.L., Tatsuta, M., Sun, J., Chin, W.: A decidable fragment in separation logic with inductive predicates and arithmetic. In: Majumdar, R., Kuncak, V. (eds.) CAV 2017, pp. 495–517 (2017). Scholar
  30. 30.
    Le, T.C., Zheng, G., Nguyen, T.: SLING: using dynamic analysis to infer program invariants in separation logic. In: McKinley, K.S., Fisher, K. (eds.) PLDI 2019, pp. 788–801 (2019).
  31. 31.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010, pp. 348–370 (2010). Scholar
  32. 32.
    Li, Y., Tarlow, D., Brockschmidt, M., Zemel, R.S.: Gated graph sequence neural networks. CoRR abs/1511.05493 (2015)Google Scholar
  33. 33.
    Malík, V., Hruska, M., Schrammel, P., Vojnar, T.: Template-based verification of heap-manipulating programs. In: Bjørner, N., Gurfinkel, A. (eds.) FMCAD 2018, pp. 1–9 (2018).
  34. 34.
    Miné, A.: The octagon abstract domain. High. Order. Symbolic Comput. 19(1), 31–100 (2006). Scholar
  35. 35.
    Mühlberg, J.T., White, D.H., Dodds, M., Lüttgen, G., Piessens, F.: Learning assertions to verify linked-list programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015, pp. 37–52 (2015). Scholar
  36. 36.
    O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001, pp. 1–19 (2001). Scholar
  37. 37.
    Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: ICSE, vol. 2007, pp. 75–84 (2007).
  38. 38.
    Padhi, S., Sharma, R., Millstein, T.D.: Data-driven precondition inference with learned features. In: Krintz, C., Berger, E. (eds.) PLDI 2016, pp. 42–56 (2016).
  39. 39.
    Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J.: Concolic testing heap-manipulating programs. In: FM 2019. To appearGoogle Scholar
  40. 40.
    Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J., Qin, S.: Enhancing symbolic execution of heap-based programs with separation logic for test input generation. In: ATVA 2019. To appearGoogle Scholar
  41. 41.
    Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J., Qin, S.: Testing heap-based programs with Java StarFinder. In: Chaudron, M., Crnkovic, I., Chechik, M., Harman, M. (eds.) ICSE 2018, pp. 268–269. ACM (2018).
  42. 42.
    Pham, L.H., Thi, L.T., Sun, J.: Assertion generation through active learning. In: Duan, Z., Ong, L. (eds.) ICFEM 2017, pp. 174–191 (2017). Scholar
  43. 43.
    Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 711–728 (2014). Scholar
  44. 44.
    Piskac, R., Wies, T., Zufferey, D.: GRASShopper - complete heap verification with mixed specifications. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014, pp. 124–139 (2014). Scholar
  45. 45.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, vol. 2002, pp. 55–74 (2002).
  46. 46.
    Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Appel, A.W., Aiken, A. (eds.) POPL 1999, pp. 105–118 (1999).
  47. 47.
    Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: Krintz, C., Berger, E. (eds.) PLDI 2016, pp. 491–507 (2016).

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Singapore University of Technology and DesignSingaporeSingapore
  2. 2.Singapore Management UniversitySingaporeSingapore
  3. 3.School of Computing & Digital TechnologiesTeesside UniversityMiddlesbroughUK

Personalised recommendations