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 Thibaud Lutellier
Office DC2536 DC2544
email first . last AT uwaterloo.ca first . last AT uwaterloo.ca

Important Dates (likely to change, check frequently)

Date Event
Jan 9 A1 out
Jan 27 A1 due
Jan 30 A2 out
Feb 20 - 24 Reading week
Mar 3 Mar 10 A2 due
Mar 6 Mar 13 A3 out
Mar 31 Apr 3 A3 due
Apr 3 last class

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 2)
3 Structural Coverage  
4 Data-flow Coverage
Logic Coverage		 Gay et al. Moving the Goalposts: Coverage Satisfaction is Not Enough
Gay et al. The Risks of Coverage-Directed Test Case Generation
5 Propositional Logic and SAT S. Malik and L. Zhang. Boolean Satisfiability: From Theoretical Hardness to Practical Success
D. Kroening and O. Strichman. Decision Procedures (Chapter 2)
A. Bradley and Z. Manna. The Calculus of Computation (Chapter 1)
6 Propositional Logic and SAT
First Order Logic and SMT		 A. Bradley and Z. Manna. The Calculus of Computation (Chapter 2)
L. De Moura and N. Bjorner. Satisfiability Modulo Theories: Introduction and Applications
7 First Order Logic and SMT D.R. Cok. The SMT-LIBv2 Language and Tools: A Tutorial
Z3 Tuorial
8 Symbolic Execution
Dynamic Symbolic Execution		 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
T. Avgerinos et al. Automatic Exploit Generation
Brumley et al. Unleashing MAYHEM on Binary Code
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 Dafny
Verification Condition Generation		 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 Dafny
Formal Method Tools		 K.R.M Leino and N. Polikarpova. Verified Calculation
12 Daikon
Software Model Checking		 M.D. Ernst et al. Quickly Detecting Relevant Program Invariants
V. D’Silva et al. A Survey of Automated Techniques for Formal Software Verification
13 Review  

Posts