Instructor Shmuel (Mooly) Sagiv;
TA Kalev Alpernas
Lecture Wed 16-18;
Recitation Wed 18-19
Developing correct and reliable software is considered a very difficult task. This is a unique course that teaches students novel testing and verification techniques for improving software productivity. The techniques reduce the cost of software development and improve robustness of software. These techniques have been developed in the last two decades and are becoming more mature. Many of the techniques are now implemented in research and some commercial tools.
This course focuses on pragmatical aspects. The students will gain more understanding on existing tools, their relevance, and limitations.
The techniques include:
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
08/12 There will not be a lecture on Wed 14/12.
13/01 There will be a make-up lecture and recitation today, Fri 13/01 at 11-14, in Dan David 003.
There is no exam in this course. The students must solve all homework assignment but one (40%) and then suggest an interesting project using one of the tools (60%)
Software project is a hard prerequisite and logic is soft.
| Lecture | Recitation | Exercise |
| XXX Overview | No Recitation | No assignment |
| SAT Solvers | Z3 | Graph algorithms with Z3 |
| SMT | No Recitation | No assignment |
| Bounded Model Checking | CBMC and Alloy | Use CBMC and Alloy |
| Bounded Model Checking | CBMC and Alloy | No assignment |
| Concolic Testing | KLEE | Use KLEE |
| Deductive Verification 1 | No Recitation | No assignment |
| Deductive Verification 2 and Termination | Dafny | Use Dafny |
| Interactive Deductive Verification with IVY | IVY Recitation | No assignment |
| Static Analysis 1 | No Recitation | No assignment |
| Static Analysis 2 | Chaotic Iteration | Chaotic Iteration |
| Testing | American Fuzzy Lop | Use the tools |
| Software Synthesis | TBD | TBD |
| Assignment | Submission Deadline | Grades | ||
| 1 | Z3 | 19/11 | HW 1 Grades | |
| 2 | CBMC and Alloy | 10/12 | CBMC 5.6 Installation | HW 2 Grades |
| 3 | KLEE vs. CBMC | HW 3 Grades | ||
| 4 | Dafny | 07/01 | HW 4 Grades | |
| 5 | Abstract Interpretation | HW 5 Grades |
For further information Email:msagiv@post.tau.ac.il