[talks] R Dockins general exam
mml at CS.Princeton.EDU
Thu Oct 9 14:31:29 EDT 2008
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.
Modal Separation Logic for Program Verification and Metatheory
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.
Benjamin Pierce. Types and Programming Languages. MIT Press. 2002.
Yves Bertot and Pierre Casteran. Interactive Theorem Proving and Program Development.
G.E. Hughes and J.M. Cresswell. A New Introduction to Modal Logic.
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),
More information about the talks