Formal reasoning about Software Systems 2016
Sunday 14:00-16:00 Kaplun 324
Instructor: Shmuel (Mooly) Sagiv
This seminar inspired by the course Verified System's Software given
by Benjamin Pierce.
The reliability and the safety of software systems is a long standing open problem in computer science.
Modern techniques in formal verification make it possible to apply these methods to formally verify some parts of the
system and to automatically identify bugs.
The students in the seminar will present advanced works in the subject.
List of Potential
Interesting Links to explore
A course in formal methods or compilers or logics in computer science.
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.
- 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),
- 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
- 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),
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,
A Coalgebraic Decision Procedure for NetKAT:
by Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva and Laure Thompson, POPL'15
- 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
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
- Sunday February 28, Mooly Sagiv: Introduction
- March 6, Mooly Sagiv: IVY: Interactive Safety Verification via Counterexample Generalization
- March 13, Oded Padon: Coq Tutorial
- March 20, Mooly Sagiv: Network Verification
- March 27, Mooly KLEE: KLEE: Effective Testing of Systems Programs
- April 3, Elazar Gershuni: Comprehensive Formal Verification of an OS Microkernel
- April 10, Shelly Grossman: Rehearsal: A Configuration Verification Tool for Puppet
- May 1, Omer Anson: Formal verification of a realistic compiler
- May 8, Yotam Feldman: A Design and Verification Methodology for Secure Isolated Regions
- May 15, Vadim Stotland: Ironclad
- May 22, No class
- May 29, Mooly
- June 2, Verification Day
For further information Email:email@example.com