Course Description

This course will provide an introduction to software testing and quality assurance techniques. The students will learn a wide spectrum of techniques and tools that can be used to improve and evaluate software quality ranging from mature testing methodologies to cutting edge automated verification algorithms. Topics to be covered include: coverage criteria (graph, data-flow, and logic coverage), symbolic execution (static, dynamic, concolic), constraint solving (SMT), inductive invariants, automatic deductive verification, automatic invariant synthesis, and Software Model Checking.

Additional information about the course is available in the course syllabus.

Details Instructor Teaching Assistants
Name Prof. Arie Gurfinkel (@prof_arie) Nham Le (@TA_Nham)
Office Home  
email first . last AT



Week Lecture Reading
1 Admin
2 Fault, Error, Failure
Foundations: Syntax and Semantics
H. Nielson and F. Nielson. Semantics with Applications: An Appetizer. (Chapter 1) (Chapter 2)
(Optional) C. Le Goues. The While and While3Addr Language
3 Structural Coverage
Logic Coverage
P. Ammann and J. Offutt Introduction to Software Testing
Staats et al. On the Danger of Coverage Directed Test Case Generation
4 AddressSanitizer

ATG with Fuzzing

Z3 SMT Solver
K. Serebryany et al. AddressSanitizer: A Fast Address Sanity Checker
AddressSanitizer Algorithm
AFL and libFuzzer

Z3Py Tutorial (Jupyter version)
D.R. Cok. The SMT-LIBv2 Language and Tools: A Tutorial
Z3 API Documentation on github
Z3 Python Examples
N. Bjorner et al. Programming Z3
D. Yurichev SAT/SMT by example
5 Symbolic Execution

Dynamic Symbolic Execution
J.C. King. Symbolic Execution and Program Testing

Cadar et al. Symbolic Execution for Software Testing in Practice
T. Ball and J. Daniel. Deconstructing Dynamic Symbolic Execution
R. Baldoni et al. A Survey of Symbolic Execution Techniques
- Reading Week  
6 Quiz 1
Semantics of Symbolic Execution
A. Gurfinkel. Symbolic Execution Semantics for WHILE Language
7 Propositional Logic

First Order Logic
U. Schoning. Logic for Computer Scientists (Chapter 1)
A. Bradley and Z. Manna. The Calculus of Computation (Chapter 1)

U. Schoning. Logic for Computer Scientists (Chapter 2)
A. Bradley and Z. Manna. The Calculus of Computation (Chapter 2)
8 First Order Logic (Part 2)

(SAT Solving)

Axiomatic Semantics (Part 1)

S. Malik and L. Zhang. Boolean Satisfiability: From Theoretical Hardness to Practical Success
D. Kroening and O. Strichman. Decision Procedures (Chapter 2)

H. Nielson and F. Nielson. Semantics with Applications: An Appetizer. (Chapter 9)
C.A.R. Hoare. Proof of a program: FIND
- COVID19 Pause  
9 Axiomatic Semantics (Part 2)  
10 Quiz 2
Deductive Verification with Dafny
Dafny: Tutorial
Dafny: VCGen
Dafny Tutorial (uwaterloo mirror)
J. Koening and K.R.M. Leino. Getting Started with Dafny: A Guide
K.R.M. Leino. Developing Verified Programs with Dafny
L. Herbert et al. Using Dafny, an Automatic Program Verifier
11 Verification Condition Generation
Dafny: Theorems
Dafny: Arrays
12 Dafny: Sorting  

Important Dates (likely to change, check frequently)

Jan 12 A0 out
Jan 19 A1 out
Feb 4 A1 due
Feb 2 Fuzz out
Feb 14 Fuzz due
Feb 15 - 19 Reading week
Feb 23 A2 out
Feb 23 - 27 Quiz 1
Mar 15 - 16 COVID19 Pause
Mar 17 A2 due
Mar 23 A3 out
Mar 30 Quiz 2
Apr 15 A3 due
Apr 14 Last class
Apr 21 Project Due
Apr 25 Final Exam Due