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) TBA
Office EIT 4021  
email first . last AT uwaterloo.ca

Posts

Lectures

Week Lecture Reading  
0 Admin
Introduction
A Math Primer by Andrzej Wasowski  
1 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
 
2 Foundations: Syntax and Semantics
Structural Coverage

P. Ammann and J. Offutt Introduction to Software Testing
Staats et al. On the Danger of Coverage Directed Test Case Generation
 
3 AddressSanitizer

ATG with Fuzzing
K. Serebryany et al. AddressSanitizer: A Fast Address Sanity Checker
AddressSanitizer Algorithm
AFL and libFuzzer
 
4 Symbolic Execution

J.C. King. Symbolic Execution and Program Testing
R. Baldoni et al. A Survey of Symbolic Execution Techniques
 
4 Z3 SMT Solver Z3Py Tutorial (Jupyter Notebook)
D.R. Cok. The SMT-LIBv2 Language and Tools: A Tutorial
Z3 API Documentation
z3.py on github
Z3 Python Examples
N. Bjorner et al. Programming Z3
D. Yurichev SAT/SMT by example
 
- Reading Week    
5 Dynamic Symbolic Execution 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
 
5 Semantics of Symbolic Execution A. Gurfinkel. Symbolic Execution Semantics for WHILE Language  
6 Semantics of Symbolic Execution cont.    
7 Propositional Logic
U. Schoning. Logic for Computer Scientists (Chapter 1)
A. Bradley and Z. Manna. The Calculus of Computation (Chapter 1)
 
8 First Order Logic U. Schoning. Logic for Computer Scientists (Chapter 2)
A. Bradley and Z. Manna. The Calculus of Computation (Chapter 2)
 
9 Axiomatic Semantics H. Nielson and F. Nielson. Semantics with Applications: An Appetizer. (Chapter 9)
C.A.R. Hoare. Proof of a program: FIND
 
10 Deductive Verification with Dafny
Dafny: Tutorial
Dafny: VCGen
Dafny Tutorial (uwaterloo mirror) (in class examples)
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)

Sep 8 A0 out
Sep 11 A0 due
Sep 11 A1 out
Sep 25 Fuzz out
Oct 6 A1 due
Oct 9 - 13 Reading week
Oct 27 Fuzz due
Oct 23 A2 out
Nov 10Nov 15 A2 due
Nov 13 A3 out
Dec 5 A3 due
Dec 4 Last class
Dec 18 Project Due

Previous course websites

2019 2020 2021 2022