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 uwaterloo.ca

Posts

Lectures

Week Lecture Reading
1 Admin
Introduction
 
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][logic]
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
K. Serebryany et al. AddressSanitizer: A Fast Address Sanity Checker
AddressSanitizer Algorithm
AFL and libFuzzer
5 Symbolic Execution

J.C. King. Symbolic Execution and Program Testing
R. Baldoni et al. A Survey of Symbolic Execution Techniques
5 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  
6 Quiz 1
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
7 Semantics of Symbolic Execution

Propositional Logic
A. Gurfinkel. Symbolic Execution Semantics for WHILE Language

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)
- COVID19 Pause  
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 Quiz 2
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)

Jan 12 A0 out
Jan 19 A1 out
Feb 4 A1 due
Feb 2 Fuzz out
Feb 14 (Feb 22) Fuzz due
Feb 15 - 19 Reading week
Feb 23 A2 out
Feb 23 - 27 Quiz 1
Mar 15 - 16 COVID19 Pause
Mar 18 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