ECE.453/CS.447/CS.647 Software Testing, Quality Assurance, and Maintenance

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 Hari Govind VK
Office DC2522  
email first . last AT uwaterloo.ca —

Posts

Lectures

Week Lecture Reading
1 Admin
Introduction
Fault, Error, Failure		  
2 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
z3.py 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
6 Semantics of Symbolic Execution
Quiz 1		 A. Gurfinkel. Symbolic Execution Semantics for WHILE Language
- Reading Week  
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
9 Axiomatic Semantics (Part 2)  
- COVID19 Break  
10 Deductive Verification with Dafny 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
10 Verification Condition Generation  

Important Dates (likely to change, check frequently)

Jan 13 A1 out
Jan 31 A1 due
Feb 3 A2 out
Feb 14 Quiz 1
Feb 17 - 21 Reading week
Mar 6 A2 due
Mar 9 A3 out
Mar 9 NO LECTURE
Mar 20 Quiz 2
Apr 3 A3 due
Apr 3 Last class