Time: Tue, 2PM—3PM

Location: WVH 462

Group leader (23spring): Isaac Khor

Topic: Systems Verification

22 fall

Candidate papers:

Program verification (”how to write bug-free code”)

• WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems, SoCC 19 https://dl.acm.org/doi/10.1145/3357223.3362739
• Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems, OOPSLA 21 https://dl.acm.org/doi/10.1145/3485474
• IronFleet: Proving Practical Distributed Systems Correct, SOSP 15 https://www.microsoft.com/en-us/research/wp-content/uploads/2015/10/ironfleet.pdf
• Verdi: A Framework for Implementing and Verifying Distributed Systems, PLDI 15 https://verdi.uwplse.org/verdi.pdf
• I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols, SOSP 19 https://web.eecs.umich.edu/~barisk/public/i4.pdf
• seL4: Formal Verification of an OS Kernel, SOSP 09 https://dl.acm.org/doi/10.1145/1629575.1629596
• CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels, OSDI 16 https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu
• Hyperkernel: Push-Button Verification of an OS Kernel, SOSP 17 https://unsat.cs.washington.edu/papers/nelson-hyperkernel.pdf
• Using Crash Hoare Logic for Certifying the FSCQ File System, SOSP 15 https://pdos.csail.mit.edu/papers/fscq:sosp15.pdf
• Verifying concurrent, crash-safe systems with Perennial, SOSP 19 https://www.chajed.io/papers/perennial:sosp2019.pdf
• Push-Button Verification of File Systems via Crash Refinement, OSDI 16 https://www.usenix.org/system/files/conference/osdi16/osdi16-sigurbjarnarson.pdf

Execution Integrity or verifiable computation (”how to ensure code runs as written”)