Techniques for Improving Software Productivity

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:

Testing Tools

Symbolic Tools and Verification

Z3 python interface tutorial

Dafny

IVy

Sketch

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

Contents

Notifications

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.

Requirements

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.

Course Schedule

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

Homework Assignments

Homework assignments submission instructions.

Source code repository, containing the examples shown in the recitations, and code skeletons for the assignments.

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 17/12 24/12 28/12 HW 3 Grades
4 Dafny 07/01 HW 4 Grades
5 Abstract Interpretation 23/01 28/01

Linux VM For Running The Homework

Last Updated: 19/01/17

Disclaimer: This VM is provided for your convenience only.
It is not necessary for running the examples - you are free to install the tools we use throught the semester on your own computers and run the assignments that way.
We will not provide any kind of support for the VM.

To download a Linux VM click here and enter the following:
Claim ID: WGFSRHPSmQbhP6KV
Claim Passcode: uJzAkDUcwZ52xMVs

VM Username: softprod
VM Password (also for sudo): softprod

Note: This is a very big download (~4GB). We suggest you download it on campus, over one of the University's WiFi networks.

Course Forum

You can find the course forum here.

Example Exam

An example exam can be found here.

For further information Email:msagiv@post.tau.ac.il