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 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 |
Quiz 1 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 |
(Required) L. De Moura and N. Bjorner. Satisfiability Modulo Theories: Introduction and Applications
(Required) 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 |
Verification Condition Generation |
K.R.M Leino and N. Polikarpova. Verified Calculation |
11 |
Quiz 2 NO CLASS Dafny: Arrays |
|
12 |
Dafny: Sort Formal Method Tools Good Friday |
|
13 |
Last week |
|