Automatic Software Verification

Tuesday 17-20, Shenkar-Physics 105
Instructor: Mooly Sagiv
TA: Oded Padon (odedp@mail.tau.ac.il)

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

• Vijay D'Silva, Daniel Kroening, and Georg Weissenbacher: A Survey of Automated Techniques for Formal Software Verification
• Alex Aiken, David Dill, Clark Barrett,Manolis Papadakis: CS357: Techniques for Program Analysis and Verification
• Isil Dillig: Automated Logical Reasoning
• Aaron Bradley and Zohar Manna: The Calculus of Computations
• Patrick Cousot: Introduction to Abstract Interpretation
• Bruno Blanchet: Introduction to Abstract Interpretation

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

• Basic
• Advanced
• Strategies
• Fixed-Points

Exercises

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

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