CSE 599W is a special topics course on systems verification.
We will examine research papers on applying
formal verification techniques to building provably correct
software, such as compilers, operating systems, Web browsers,
and distributed systems.
We expect you to present and discuss papers during lectures,
finish a set of assignments,
work on a research project,
and make a presentation of your project at the end of the quarter.
Reading list ideas
- Viola: Trustworthy Sensor Notifications for Enhanced Privacy on Mobile Systems, MobiSys 2016
- Cogent: Verifying High-Assurance File System Implementations, ASPLOS 2016
- IronFleet: Proving Practical Distributed Systems Correct, SOSP 2015
- Using Crash Hoare Logic for Certifying the FSCQ File System, SOSP 2015
- Verified Correctness and Security of OpenSSL HMAC, USENIX Security 2015
- Verdi: A Framework for Implementing and Formally Verifying Distributed Systems, PLDI 2015
- Efficient Synthesis of Network Updates, PLDI 2015
- Deep Specifications and Certified Abstraction Layers, POPL 2015
- Developing Correctly Replicated Databases Using Formal Tools, DSN 2014
- Ironclad Apps: End-to-End Security via Automated Full-System Verification, OSDI 2014
- Jitk: A Trustworthy In-Kernel Interpreter Infrastructure, OSDI 2014
- Automating Formal Proofs for Reactive Systems, PLDI 2014
- Comprehensive Formal Verification of an OS Microkernel, TOCS 2014
- NetKAT: Semantic Foundations for Networks, POPL 2014
- Implementing TLS with Verified Cryptographic Security, Oakland 2013
- RockSalt: Better, Faster, Stronger SFI for the x86, PLDI 2012
- Establishing Browser Security Guarantees through Formal Shim Verification, USENIX Security 2012
- Header Space Analysis: Static Checking For Networks, NSDI 2012
- Trace Based Verification of Imperative Programs with I/O, Journal of Symbolic Computation, 2011
- Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System, PLDI 2010
- Toward a Verified Relational Database Management System, POPL 2010
- A Formally Verified Compiler Back-end, Journal of Automated Reasoning, 2009
- Extended Static Checking for Java, PLDI 2002
- Safe Kernel Extensions Without Run-Time Checking, OSDI 1996
- Proving the Correctness of Heuristically Optimized Code, CACM 1978
Links