Automatic Software Verification
Tuesday 17-20, Shenkar-Physics 105
Instructor: Mooly Sagiv
TA: Oded Padon (firstname.lastname@example.org)
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)
- 10/3 Introduction: Why verify your software: Rice Theorem and some techniques
Scribe by Shelly Grossman, Adi Gilboa, Itay Polack
- 20/3 10-13 (Election Make-Up class) SAT Solvers for propositional logic
Scribe by Kalev Alpernas
- 24/3 Beyond propositional logic: SMT Solvers
Scribe by Asya Frumkin and Aviv Kuvent
- 14/4 Deductive Verification using SMT
Scribe by Nimrod Busany and Yotam Frank
- 21/4 Concolic Executions: combining dynamic and symbolic executions
Scribe by Omer Anson
- 28/4 Bounded Model Checking
Scribe by Amit Lichtenberg
- 28/4 Introduction to Abstract Interpretation
Scribe by Oded Elbaz
- 5/5 Theory of Program Analysis
Scribe by Oleg Zlydenko and Ofir Geri
- 12/5 Some Applications of Abstract Interpretations
- 19/5 Applications to Shape Analysis
- 26/5 Counter Example Guided Refinement
- 2/6 Procedures
- 9/6 IC3 / PDR
- 19/6 10:00-13:00 Research from Tel-Aviv and Cool Verification
Course source code
repository contains source code from the class demos and source
code needed for the exercises.
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
- SAT & SMT Due
- Abstract Interpretation Due 16/06/2015
If your POWERPOINT does not show certain
mathematical characters use fonts in a zip file, by clicking
Make sure to extract
them to the appropriate directory,
Alternatively, you can extract them anywhere, and install them via the