Rob Dockins will present his research seminar/general exam on Thursday October 16 at 3PM in Room 402. The members of his committee are: Andrew Appel (advisor), David Walker, and Brian Kernighan. 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. ------------------------------------ Title: Modal Separation Logic for Program Verification and Metatheory Abstract: The construction of new logics for reasoning about programs has a long history in the field of program verification, going back at least to the seminal works of Floyd and Hoare. In this talk, I shall show how to combine separation logic with a generic multimodal logic using the proof assistant Coq. The logic that results is useful as a substrate for building higher-level program logics and as a tool for proving metatheoretic properties. The techniques I present can be readily generalized across different programming languages and support a large collection of features including mutable memory, unstructured control flow, explicit memory management, and shared-memory concurrency. I present examples from a toy language, the list machine benchmark, and from Concurrent C Minor, a realistic intermediate language for a concurrent C compiler. Reading List: Books: Benjamin Pierce. Types and Programming Languages. MIT Press. 2002. Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development. Springer. 2004. G.E. Hughes and J.M. Cresswell. A New Introduction to Modal Logic. Routldge. 1996. Papers: Andrew W. Appel, Paul Andre Mellies, Christopher D. Richards and Jerome Vouillon. A Very Modal Model of a Modern, Major, General Type System. In Proc. Thirty-Fourth Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 2007. Chriatian Calcagno, Peter O'Hearn, Hongseok Yang. Local Action and Abstract Separation Logic. In Proc. Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS), July 2007. Alexy Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky and Mooly Sagiv. Local Reasoning for Storable Locks and Threads. In Proc. Fifth Asian Symposium on Programming Languages and Systems (APLAS), November 2007. Xavier Leroy and Sandrine Blazy. Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. Journal of Automated Reasoning, 41(1):1-31. July 2008. Greg Morrisett, David Walker, Karl Crary and Neal Glew. From System F to Typed Assembly Language. Twenty-Fifth ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 1998. Peter O'Hearn. Resources, Concurrency and Local Reasoning. Theoretical Computer Science 375(1):271-307, May 2007. Vaughan R. Pratt. Application of Modal Logic to Programming. Studia Logica, 39(2-3):257-274. June, 1980. John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. Seventeenth Annual IEEE Symposium on Logic in Computer Science (LICS), July 2002.