Committee

  • Andrew Appel (advisor)
  • Zak Kincaid
  • Aarti Gupta

Title

Decision procedures useful in separation-logic proofs of functional correctness

Abstract

VST has been used successfully to verify C programs with rich specifications. However, proofs in Verifiable C require substantial human work, which prevents applications in larger programs. We have improved VST’s proof automation in two ways. The first is term inference in existential variables, heap lemmas and function calls. The second is an automatic prover that solves relations on lists. Our list/array theory contains list concatenations, which occur frequently in array content specifications, and are undecidable in general. But we show a decidable fragment, in which relations between different positions in the same list are prohibited. We show this fragment covers many useful verification goals found in existing VST verifications.

Reading List

  1. Bradley, Aaron R., and Zohar Manna. The calculus of computation: decision procedures with applications to verification. Springer Science & Business Media, 2007.
  2. Pierce, Benjamin C., et al. "Software foundations." Volumes 1 & 2. Web page (2010).
  3. Bradley, Aaron R. "Safety analysis of systems." Chapter 2. PhD diss., Stanford University, 2007.
  4. Habermehl, Peter, Radu Iosif, and Tomáš Vojnar. "What else is decidable about integer arrays?." International Conference on Foundations of Software Science and Computational Structures. Springer, Berlin, Heidelberg, 2008.
  5. Lothaire, Monsieur, and M. Lothaire. Algebraic combinatorics on words. Chapter 12. Cambridge university press, 2002.
  6. Furia, Carlo A. "What’s Decidable About Sequences?." International Symposium on Automated Technology for Verification and Analysis. Springer, Berlin, Heidelberg, 2010.
  7. Le, Xuan-Bach, and Aquinas Hobor. "Logical reasoning for disjoint permissions." European Symposium on Programming. Springer, Cham, 2018.
  8. Jacobs, Bart, et al. "VeriFast: A powerful, sound, predictable, fast verifier for C and Java." NASA Formal Methods Symposium. Springer, Berlin, Heidelberg, 2011.
  9. Calcagno, Cristiano, et al. "Compositional shape analysis by means of bi-abduction." ACM SIGPLAN Notices. Vol. 44. No. 1. ACM, 2009.
  10. Brotherston, James, Nikos Gorogiannis, and Max Kanovich. "Biabduction (and related problems) in array separation logic." International Conference on Automated Deduction. Springer, Cham, 2017.
  11. Appel, Andrew W. "VeriSmall: verified smallfoot shape analysis." International Conference on Certified Programs and Proofs. Springer, Berlin, Heidelberg, 2011.