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 first . last AT



Week Lecture Reading
1 Admin
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 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

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

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