Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11893))

Included in the following conference series:

Abstract

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 is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Facebook Infer. https://fbinfer.com

  2. https://figshare.com/s/ba1c12ad90c138fbb240

  3. https://github.com/sunjun-group/Ziyuan

  4. Albarghouthi, A., Berdine, J., Cook, B., Kincaid, Z.: Spatial interpolants. In: Vitek, J. (ed.) ESOP 2015, pp. 634–660 (2015). https://doi.org/10.1007/978-3-662-46669-8_26

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-642-31424-7_16

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-642-22110-1_16

    Chapter  Google Scholar 

  7. Brockschmidt, M., Chen, Y., Kohli, P., Krishna, S., Tarlow, D.: Learning shape analysis. In: Ranzato, F. (ed.) SAS 2017, pp. 66–87 (2017). https://doi.org/10.1007/978-3-319-66706-5_4

    Chapter  Google Scholar 

  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). https://doi.org/10.1145/290179.290184

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1145/2049697.2049700

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1016/j.scico.2010.07.004

    Article  MATH  Google Scholar 

  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). https://doi.org/10.1145/1062455.1062522

  12. Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: Harris, G.E. (ed.) OOPSLA 2008, pp. 213–226 (2008). https://doi.org/10.1145/1449764.1449782

  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). https://doi.org/10.1007/978-3-642-22110-1_29

    Chapter  Google Scholar 

  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). https://doi.org/10.1016/j.scico.2007.01.015

    Article  MathSciNet  MATH  Google Scholar 

  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). https://doi.org/10.1007/3-540-45251-6_29

    Google Scholar 

  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). https://doi.org/10.1007/978-3-642-39799-8_57

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-08867-9_5

    Chapter  Google Scholar 

  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). https://doi.org/10.1145/2837614.2837664

  19. Ginsburg, S., Spanier, E.: Semigroups, presburger formulas, and languages. Pac. J. Math. 16(2), 285–296 (1966)

    Article  MathSciNet  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-21690-4_20

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-662-54580-5_24

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-642-39799-8_52

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-08867-9_3

    Chapter  Google Scholar 

  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). https://doi.org/10.1145/2983990.2984023

  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). https://doi.org/10.1007/978-3-319-08867-9_4

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-41528-4_21

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-89960-2_3

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-63390-9_26

    Chapter  Google Scholar 

  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). https://doi.org/10.1145/3314221.3314634

  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).https://doi.org/10.1007/978-3-642-17511-4_20

    Chapter  Google Scholar 

  32. Li, Y., Tarlow, D., Brockschmidt, M., Zemel, R.S.: Gated graph sequence neural networks. CoRR abs/1511.05493 (2015)

    Google Scholar 

  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). https://doi.org/10.23919/FMCAD.2018.8603009

  34. Miné, A.: The octagon abstract domain. High. Order. Symbolic Comput. 19(1), 31–100 (2006). https://doi.org/10.1007/s10990-006-8609-1

    Article  MATH  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-22969-0_3

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/3-540-44802-0_1

    Google Scholar 

  37. Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: ICSE, vol. 2007, pp. 75–84 (2007). https://doi.org/10.1109/ICSE.2007.37

  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). https://doi.org/10.1145/2908080.2908099

  39. Pham, L.H., Le, Q.L., Phan, Q.S., Sun, J.: Concolic testing heap-manipulating programs. In: FM 2019. To appear

    Google Scholar 

  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 appear

    Google Scholar 

  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). https://doi.org/10.1145/3183440.3194964

  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). https://doi.org/10.1007/978-3-319-68690-5_11

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-319-08867-9_47

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-642-54862-8_9

    Chapter  Google Scholar 

  45. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, vol. 2002, pp. 55–74 (2002). https://doi.org/10.1109/LICS.2002.1029817

  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). https://doi.org/10.1145/292540.292552

  47. Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: Krintz, C., Berger, E. (eds.) PLDI 2016, pp. 491–507 (2016). https://doi.org/10.1145/2908080.2908125

Download references

Acknowledgments

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

Author information

Authors and Affiliations

  1. Singapore University of Technology and Design, Singapore, Singapore

    Long H. Pham

  2. Singapore Management University, Singapore, Singapore

    Jun Sun

  3. School of Computing & Digital Technologies, Teesside University, Middlesbrough, UK

    Quang Loc Le

Authors
  1. Long H. Pham
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jun Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Quang Loc Le
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Long H. Pham .

Editor information

Editors and Affiliations

  1. University of Kaiserslautern, Kaiserslautern, Germany

    Anthony Widjaja Lin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Pham, L.H., Sun, J., Le, Q.L. (2019). Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning. In: Lin, A. (eds) Programming Languages and Systems. APLAS 2019. Lecture Notes in Computer Science(), vol 11893. Springer, Cham. https://doi.org/10.1007/978-3-030-34175-6_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34175-6_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34174-9

  • Online ISBN: 978-3-030-34175-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation