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	Jakub Kuderski and Qian (David) Liang
Office	DC2536
email	first . last AT uwaterloo.ca	first . last AT uwaterloo.ca

Posts

• 03 Mar 2019 » Dafny Ref
• 03 Mar 2019 » Dafny Quick Reference
• 19 Jan 2019 » (Archived) Z3Py Tutorial
• 19 Jan 2019 » Docker installation on Windows OS
• 07 Jan 2019 » Mounting code from a local directory into a docker container
• 02 Jan 2019 » Setting up virtualenv
• 02 Jan 2019 » Setting up VirtualBox
• 02 Jan 2019 » Learning Python

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 D.R. Cok. The SMT-LIBv2 Language and Tools: A Tutorial Interactive Z3 Tuorial Z3 API Documentation z3.py on github Z3 Python Examples
5	Symbolic Execution Dynamic Symbolic Execution Semantics of 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 A. Gurfinkel. Symbolic Execution Semantics for WHILE Language
6	Quiz 1
7	Propositional Logic SAT Solving	U. Schoning. Logic for Computer Scientists (Chapter 1) A. Bradley and Z. Manna. The Calculus of Computation (Chapter 1) S. Malik and L. Zhang. Boolean Satisfiability: From Theoretical Hardness to Practical Success D. Kroening and O. Strichman. Decision Procedures (Chapter 2)
8	First Order Logic SMT	U. Schoning. Logic for Computer Scientists (Chapter 2) A. Bradley and Z. Manna. The Calculus of Computation (Chapter 2) L. De Moura and N. Bjorner. Satisfiability Modulo Theories: Introduction and Applications
9	Axiomatic Semantics Dafny	H. Nielson and F. Nielson. Semantics with Applications: An Appetizer. (Chapter 9) C.A.R. Hoare. Proof of a program: FIND Dafny Tutorial 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	Quiz 2 Dafny: Tutorial Dafny: VCGen
11	Verification Condition Generation Dafny: Theorems Dafny: Arrays	K.R.M Leino and N. Polikarpova. Verified Calculation
12	Dafny: Sorting Dynamic Discovery of Likely Invariants Verification tools in practice	M.D. Ernst et al. Quickly Detecting Relevant Program Invariants

Important Dates (likely to change, check frequently)

Jan 14	A1 out
Feb 1	A1 due
Feb 4	A2 out
Feb 11 Feb 13	Quiz 1
Feb 18 - 22	Reading week
Mar 8	A2 due
Mar 11	A3 out
Mar 18	Quiz 2
Apr 5	A3 due
Apr 5	Last class