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.


  • Prerequisites
  • Requirements
  • List of Potential Papers
  • Schedule
  • Interesting Links to explore 
  • Prerequisites

        A course in formal methods or compilers or logics in computer science.

    Seminar Requirements

    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

    Reasoning about Distributed Protocols

    Operating Systems

    Network and Cloud Verification and Synthesis




    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
    11. May 22, No class
    12. May 29, Mooly
    13. June 2, Verification Day

    Interesting Links

    For further information