ECE.653 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 Assistant
Name Prof. Arie Gurfinkel TBD
Office DC2536  
email first . last AT uwaterloo.ca first . last AT uwaterloo.ca

Posts

Lectures

Week Lecture Reading
1 Admin
Introduction
Fault, Error, Failure		  
2 Foundations: Syntax and Semantics C. Le Goues. The While and While3Addr Language
H. Nielson and F. Nielson. Semantics with Applications: An Appetizer. (Chapter 1) (Chapter 2)
3 Structural Coverage P. Ammann and J. Offutt Introduction to Software Testing
4 Data-flow Coverage
Logic Coverage



Z3 SMT Solver
(Required) Staats et al. On the Danger of Coverage Directed Test Case Generation
Hayhurst et al. A Practical Tutorial on Modified Condition/Decision Coverage
Gay et al. Moving the Goalposts: Coverage Satisfaction is Not Enough
Gay et al. The Risks of Coverage-Directed Test Case Generation
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		 (Required up to Section 5) J.C. King. Symbolic Execution and Program Testing
A. Gurfinkel Symbolic Execution Semantics for WHILE Language
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

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)
7 SAT Solving

First Order Logic		 S. Malik and L. Zhang. Boolean Satisfiability: From Theoretical Hardness to Practical Success
D. Kroening and O. Strichman. Decision Procedures (Chapter 2)
U. Schoning. Logic for Computer Scientists (Chapter 2)
A. Bradley and Z. Manna. The Calculus of Computation (Chapter 2)
8 SMT
Automatic Exploit Generation

Axiomatic Semantics		 L. De Moura and N. Bjorner. Satisfiability Modulo Theories: Introduction and Applications
T. Avgerinos et al. Automatic Exploit Generation
D. Brumley et al. Unleashing MAYHEM on Binary Code
H. Nielson and F. Nielson. Semantics with Applications: An Appetizer. (Chapter 9)
C.A.R. Hoare. Proof of a program: FIND
9 Axiomatic Semantics
Dafny
 (required) H. Nielson and F. Nielson. Semantics with Applications: An Appetizer. (Chapter 9)
(required) Dafny Tutorial
(required) 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: Lemmas
Dafny: VCGen
K.R.M Leino and N. Polikarpova. Verified Calculation
11 Verification Condition Generation
Dafny: Arrays
Dafny: Sorting		  
12 Formal Method Tools  

Important Dates (likely to change, check frequently)

Jan 8 A1 out
Jan 29 A1 due
Jan 29 A2 out
Feb 5 Quiz 1
Feb 19 - 23 Reading week
Mar 12 A2 due
Mar 12 A3 out
Mar 19 Quiz 2
Apr 2 last class
Apr 8 Apr 4 A3 due