Qinshi Wang will present his General Exam "Decision procedures useful in separation-logic proofs of functional correctness" on Thursday, May 9, 2019 at 3:30pm in Friend 203. The members of his committee are as follows: Andrew Appel (adviser), Zak Kincaid, and Aarti Gupta. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. Research talk 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. [ https://softwarefoundations.cis.upenn.edu/ | Webpage: https://softwarefoundations.cis.upenn.edu/ ] (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.