January 2011 - talks - lists.cs.princeton.edu

M Carroll FPO
by Melissa Lawson 20 Jan '11

20 Jan '11

Melissa Carroll will present her FPO on Wednesday January 26 at 2:30PM in Room 402. The members of her committee are: Rob Schapire, advisor; Ken Norman (PSY) and Irina Rish (IBM), readers; David Blei and Peter Ramadge (ELE), nonreaders. A copy of her thesis, "FMRI "Mind Readers": Sparsity, Spatial Structure, and Reliability", is on display in Room 310. Everyone is invited to attend her talk.

1 0

G Stewart General Exam
by Melissa Lawson 12 Jan '11

12 Jan '11

Gordon Stewart will present his research seminar/general exam on Wednesday January 19 at 2PM in Room 402. The members of his committee are: Andrew Appel 9advisor), David Walker, and David August. 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. ----------------------------------- Abstract ======== Soundness proofs of program logics such as Hoare logics and type systems are often made easier by decorating the operational semantics with information that is useful in the proof. However, modifying the operational semantics to carry around such information can make it more difficult to show that the operational semantics corresponds to what actually occurs on a real machine. In this work we present a program logic framework targeting operational semantics in Curry-style--that is, operational semantics without proof decora- tions such as separation algebras, share models, and step indexes. Although we target Curry-style operational semantics, our framework permits local reason- ing via the frame rule and retains expressive assertions in the program logic. Soundness of the program logic is derived mechanically from simple properties of primitive commands and expressions. We demonstrate our framework by deriving a separation logic for the model of a core imperative programming language with external function calls. We also apply our framework in a more realistic setting in the soundness proof of a separation logic for CompCert's Cminor. Our proofs are machine-checked in Coq. Research Papers =============== [Appel and Blazy 2007] A. W. Appel and S. Blazy. Separation logic for small- step Cminor. In 20th Intl Conference on Theorem Proving in Higher-Order Logics, pages 5-21, 2007. [Calcagno et al. 2007] C. Calcagno, P. W. O'Hearn, and H. Yang. Local ac- tion and abstract separation logic. In LICS'07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, pages 366-378, 2007. ISBN 0-7695-2908-9. doi: http://dx.doi.org/10.1109/LICS.2007.30. [Dockins et al. 2009] R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation algebras and share accounting. In The 7th Asian Symposium on Programming Languages and Systems. Springer ENTCS, 2009. URL http://msl.cs.princeton.edu/fresh-sa.pdf. [Lahiri 2008] S. Lahiri, S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In POPL'08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008. [Lerner 2003] S. Lerner, T. Millstein, and C. Chambers. Automatically Proving the Correctness of Compiler Optimizations. In PLDI'03: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2003. [Leroy 2009] X. Leroy. Formal verification of a realistic compiler. Communica- tions of the ACM, 52(7):107-115, 2009. [Leroy and Blazy 2008] X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. J. Au- tomated Reasoning, 41(1):1-31, 2008. [Necula 1997] G. Necula. Proof-Carrying Code. In POPL'97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997. [Parkinson 2010] M. Parkinson. The next 700 separation logics. In G. Leavens, P. O'Hearn, and S. Rajamani, editors, Verified Software: Theories, Tools, Experiments, volume 6217 of Lecture Notes in Computer Science, pages 169-182. Springer Berlin / Heidelberg, 2010. [Parkinson et al. 2006] M. Parkinson, R. Bornat, and C. Calcagno. Variables as resource in Hoare logics. Proc. of 21st Annual IEEE Symp. on Logic in Computer Science, 0:137-146, 2006. ISSN 1043-6871. [Reynolds 2002] 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. Textbooks ========= [Pierce 2002] B. Pierce. Types and Programming Languages. 2002. [Winskell 1993] G. Winskell. The Formal Semantics of Programming Languages (Chapters 1-7). 1993.

1 0

W Josephson FPO
by Melissa Lawson 04 Jan '11

04 Jan '11

William Josephson will present his FPO on Tuesday January 11 at 2:30 PM in Room 302 (note Room!) The members of his committee are: Kai Li, advisor; Jen Rexford and Brian Kernighan, readers; Mike Freedman and Doug Clark, nonreaders. A copy of his thesis, "A Direct-Access File System for a New Generation of Flash Memory", is on display in Room 310. Everyone is invited to attend his talk.

1 0