Automatic Software Verification

Tuesday 17-20, Shenkar-Physics 105
Instructor: Mooly Sagiv
TA: Oded Padon (

Our daily life is affected by the correctness of software systems. Software bugs can cost enormous amount of money and can be exploited by malicious users to gain control of your computer.

We will study various techniques that can be used to identify software bugs at compile-time and to prove the absence of certain kinds of bugs.

Prerequisites: Computer Models and Software Project.

The grade of the course will be based on 10% Course notes, 45% homework assignments, and 45% exam or project.

This course is inspired by CS395T: Automated Logical Reasoning (UT Austin) taught by Isil Dillig

Some Reading Material

Tentative Schedule (To be changed during the term based on student's feedback)

  1. 10/3 Introduction: Why verify your software: Rice Theorem and some techniques
    Scribe by Shelly Grossman, Adi Gilboa, Itay Polack
  2. 20/3 10-13 (Election Make-Up class) SAT Solvers for propositional logic
    Scribe by Kalev Alpernas Elizabeth Firman
  3. 24/3 Beyond propositional logic: SMT Solvers
    Scribe by Asya Frumkin and Aviv Kuvent
  4. 14/4 Deductive Verification using SMT
    Scribe by Nimrod Busany and Yotam Frank
  5. 21/4 Concolic Executions: combining dynamic and symbolic executions
    Scribe by Omer Anson
  6. 28/4 Bounded Model Checking
    Scribe by Amit Lichtenberg
  7. 28/4 Introduction to Abstract Interpretation
    Scribe by Oded Elbaz
  8. 5/5 Theory of Program Analysis
    Scribe by Oleg Zlydenko and Ofir Geri
  9. 12/5 Some Applications of Abstract Interpretations
  10. 19/5 Applications to Shape Analysis
  11. 26/5 Counter Example Guided Refinement
  12. 2/6 Procedures
  13. 9/6 IC3 / PDR
  14. 19/6 10:00-13:00 Research from Tel-Aviv and Cool Verification

Online Resources

Course source code repository contains source code from the class demos and source code needed for the exercises.

Course forum is the place for questions and discussions about course material and exercises, and also annoucments from the course staff (please join the forum).

Z3 python interface tutorial

We covered most of the first two in the recitation:


Exercise submission guidelines

  1. SAT & SMT Due 21/04/2015 28/04/2015
  2. Abstract Interpretation Due 16/06/2015


Home Exam

Important Message

If your POWERPOINT does not show certain mathematical characters use fonts in a zip file, by clicking here. Make sure to extract
them to the appropriate directory,

Alternatively, you can extract them anywhere, and install them via the control panel