Techniques for Improving Software Productivity

Instructor Shmuel (Mooly) Sagiv; TA Kalev Alpernas
Lecture Sun 16-18, Orenstein 110; Recitation Sunday 18-19, Orenstein 110

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

Requirements

The students must solve all homework assignment but one (40%) and then complete an exam (60%)

Software project and logic are hard prerequisites.

Course Schedule

Lecture Recitation Exercise
Overview PPTX
SAT Solvers PPTX Sat in Z3 Use Z3
SMT PPTX SMT in Z3
Bounded Model Checking PPTX CBMC Use CBMC and Alloy
Bounded Model Checking Alloy
Concolic Testing PPTX KLEE Use KLEE
Deductive Verification PPTX
Deductive Verification 2 and Termination Dafny Use Dafny
Interactive Deductive Verification with IVY PPTX IVY Recitation
Static Analysis 1 PPTX
Static Analysis 2 PPTX Chaotic Iteration Chaotic Iteration
Shape Analysis PPTX American Fuzzy Lop
Software Synthesis Sketch

Homework Assignments

Homework assignments submission instructions (Updated 19-03-19).

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

Grades will be updated in this document (requires tau mail account login). Last updated: Grades for Assignment 1

Assignment Submission Deadline
1 Z3 31/03
2 CBMC and Alloy 14/04 21/04
3 KLEE vs. CBMC 28/04 05/05
4 Dafny 19/05
5 Abstract Interpretation 12/06 19/06

Linux VM For Running The Homework

Last Updated: 11/03/19

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.

Checksum: (you can use 7-zip to calculate the checksum) 

---------------------------
Checksum information
---------------------------
Name: Verification-Box.zip
Size: 7065651261 bytes (6738 MB)

CRC32: 7E1C2B7A

CRC64: 5B2E560B2A2C6AA2

SHA256: E363F42785C8964C9C7A5BA9068C4ADF7C4F57C4083F008B2E4FAC8098A5AE57

SHA1: F952429ADFA4A0F016248DFA35E68AA64F50102D

BLAKE2sp: 9E4061F8240713EC8E5AA1D8D3132333051DE0E8EE0482050ABE6E5304C9A029

---------------------------
OK
---------------------------
VM Username: verifier
VM Password (also for sudo): verifier

Note: This is a very big download (~7GB). 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

Example exams can be found here and here.

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