Qinxiang Cao will present his Generals on May 18, 2015 at 1:30PM in CS 302. The members of his committee are as follows: Andrew Appel (adviser), Aarti Gupta, and David Walker. Abstract: Program Verification on Aggregate Types in C. Verifiable Software Toolchain (VST) is a verified tool to prove the full functional correctness of C programs. As introduced by Hoare logic, pre/post conditions are used in VST to specify program behaviors. And these specifications can be proved by applying Hoare rules. However, when aggregate C types are involved, pre/post conditions become messy. Users need to write (assertion) conjuncts for every field of a struct type in pre/post conditions. Since structs, unions and arrays can be nested together arbitrarily in C, this leads to very verbose assertions. In this work, we define a spatial predicate to describe aggregate-typed data more concisely. Then we define concise (derived) Hoare rules about loading/storing on aggregate data types. All these rules are compatible with the separation logic settings in VST. As our assertion predicate on aggregate types has to be dependently typed, we carefully designed the type system such that users do not need to worry about Coq's type checking issue. Text books: Michael Huth, Mark Ryan. Logic in Computer Scienc, Modelling and Reasoning about Systems. 2004. B. Pierce. Types and Programming Languages. 2002. Papers and Book Chapters: [Reynolds] J.C. Reynolds. Separation Logic: a Logic for Shared Mutable Data Structures. In LICS’02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 55 - 74, 2002. [Stephen Brookes] A semantics for concurrent separation logic. In Theoretical Computer Science, Volume 375, Issues 1–3, 1 May 2007, Pages 227–270 [Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, Jérôme Vouillon] A very modal model of a modern, major, general type system. In POPL 20007. [A. W. Appel] VeriSmall: Verified Smallfoot Shape Analysis. In First International Conf. on Certified Programs and Proofs Dec. 2011 [Yves Bertot, Pierre Casteran] Interactive Theorem Prving and Program Development. Chapter 1 - Chapter 9. [Cristiano Calcagno, Dino Distefano Peter O’Hearn Hongseok Yang] Compositional Shape Analysis by means of Bi-Abduction [Dirk van Dalen] Intuitionistic Logic. In Logics and Structures, Chapter 5, 1994 [Ranjit Jhala, Rupak Majumdar] Software model checking. ACM Computing Surveys 41(4) (2009)