Prerequisites

Seminar Requirements

• Select three articles by Sunday 6/3
• Read the article before presenting your paper
• Participate in seminar talks (can miss one)
• Present a paper on Tueday to Mooly (Schriber 317) and Sunday in class

List of Papers

All the articles can be located in the internet using a search engine. Please use most updated version. Please also download and play with any other available material. Please do not use author's slides. For papers at PLDI'16, I can arrange to receive drafts.

Compiler Verification

• Formal verification of a realistic compiler: Xavier Leroy, CACM 2009.
• Provably Correct Peephole Optimizations with Alive: Nuno P. Lopes, David Menendez, Santosh Nagarakatte, John Regehr, PLDI'2015
• Lightweight Verification of Separate Compilation: Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis, POPL'16

Reasoning about Distributed Protocols

• IronFleet: Proving Practical Distributed Systems: Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, Brian Zill (Microsoft Research), SOSP'15
• Verdi: A Framework for Formally Verifying Distributed System Implementations: James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, Thomas Anderson, PLDI'15

Operating Systems

• Comprehensive Formal Verification of an OS Microkernel: Klein et al, TOCS 2014.
• Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System, Yang et al, PLDI/2010
• Ironclad Apps: End-to-End Security via Automated Full-System Verification, Hawblitzel et al, OSDI 2014.
• Using Crash Hoare Logic for Certifying the FSCQ File System: Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich (MIT CSAIL), SOSP'15
• Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock: Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. OSDI 2014: 33-47 SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems: Tom Ridge (University of Leicester), David Sheets (University of Cambridge), Thomas Tuerk (FireEye), Andrea Giugliano (University of Leicester), Anil Madhavapeddy, Peter Sewell (University of Cambridge), SOSP'15
• Cross-checking Semantic Correctness: The Case of Finding File System Bugs: Changwoo Min, Sanidhya Kashyap, Byoungyoung Lee, Chengyu Song, Taesoo Kim (Georgia Institute of Technology)

Network and Cloud Verification and Synthesis

• Nuno P. Lopes, Nikolaj Bjorner, Patrice Godefroid, Karthick Jayaraman, George Varghese: Checking Beliefs in Dynamic Networks, NSDI 2015: 499-512
• Rehearsal: A Configuration Verification Tool for Puppet: Rian Shambaugh, Aaron Weiss, Arjun Guha, PLDI'16
• BUZZ: Testing Context-Dependent Policies in Stateful Networks: Seyed K. Fayaz, Tianlong Yu, Yoshiaki Tobioka, Sagar Chaki, and Vyas Sekar, Carnegie Mellon University, NSDI'16
• A Coalgebraic Decision Procedure for NetKAT: by Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva and Laure Thompson, POPL'15

Misc

• Verification of a Cryptographic Primitive: SHA-256: Andrew Appel, PLDI'15, TOPLAS
• A Formal C Memory Model Supporting Integer-Pointer Casts: Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis, PLDI'15
• KJS: A Complete Formal Semantics of JavaScript: Daejun Park, Andrei Stefanescu, Grigore Rosu
• A Design and Verification Methodology for Secure Isolated Regions: Rohit Sinha, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram Rajamani, Sanjit Seshia, Kapil Vaswani, PLDI'16
• Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz: Verifying Safety Properties with the TLA+ Proof System:IJCAR 2010: 142-148

Schedule

1. Sunday February 28, Mooly Sagiv: Introduction
2. March 6, Mooly Sagiv: IVY: Interactive Safety Verification via Counterexample Generalization
3. March 13, Oded Padon: Coq Tutorial
4. March 20, Mooly Sagiv: Network Verification
5. March 27, Mooly KLEE: KLEE: Effective Testing of Systems Programs
6. April 3, Elazar Gershuni: Comprehensive Formal Verification of an OS Microkernel
7. April 10, Shelly Grossman: Rehearsal: A Configuration Verification Tool for Puppet
8. May 1, Omer Anson: Formal verification of a realistic compiler
9. May 8, Yotam Feldman: A Design and Verification Methodology for Secure Isolated Regions
10. May 15, Vadim Stotland: Ironclad
12. May 22, No class
13. May 29, Mooly
14. June 2, Verification Day

Interesting Links