Instructor |
Lecture | Date | Description | Course Materials |
---|---|---|---|
Lecture 1 | 1/15 |
Concepts: What is formal methods?
|
[Reading 0] |
Lecture 2 | 1/17 |
Concepts: Propositional logic review
|
[Reading 1] |
Lecture 3 | 1/22 |
Concepts: SAT Solvers
|
[Reading 2]
[Reading 3] |
Lecture 4 | 1/24 |
Concepts: Applications of SAT Solvers
|
Homework 1 Assigned [Reading 4] |
Lecture 5 | 1/29 |
Concepts: Introduction to SMT Solvers
|
Report project groups [Reading 5] |
Lecture 6 | 1/31 |
Concepts: DPLL Framework
|
[Reading 6] |
Lecture 7 | 2/5 |
Concepts: Finite Model Finding
|
[Reading 7] |
Lecture 8 | 2/7 |
Concepts: Alloy Modeling Language
|
[Reading 8] | Lecture 9 | 2/12 |
Concepts: Alloy Modeling Language
|
[Reading 8] |
- | 2/14 |
Concepts: Work Day
|
Homework 1 Due: by 11:59pm Homework 2 Out |
Lecture 10 | 2/19 |
Concepts: Validating Alloy Models
|
[Reading 9] |
Lecture 11 | 2/21 |
Concepts: Alloy Case Study
|
|
Lecture 12 | 2/26 |
Concepts: Hoare Logic
|
[Reading 10] |
Lecture 13 | 2/28 |
Concepts: Hoare Logic: Verification Condition Generation
|
[Reading 11] |
Lecture 14 | 3/12 |
Concepts: Verification with Dafny
|
[Reading 12] |
Lecture 15 | 3/14 |
Concepts: Bounded Verification
|
[Reading 13] [Reading 14] [Reading 15] Homework 2 Due: by 11:59pm |
Lecture 16 | 3/19 |
Concepts: Model Checking
|
[Reading 16] [Reading 17] |
- | 3/21 | Honors convocation: No class | Homework 3 Out |
Lecture 17 | 3/26 |
Concept: Model Checking
|
[Reading 18] |
Lecture 18 | 3/28 |
Concepts: Symbolic Execution
|
[Reading 19] [Reading 20] |
Lecture 19 | 4/2 |
Concept: Concolic Execution
|
[Reading 21] [Reading 22] |
- | 4/4 | No Class: Project Work Day | |
Lecture 20 | 4/9 |
Concept: Program Synthesis
|
[Reading 23] |
Lecture 21 | 4/11 |
Concepts: Program Synthesis by Enumeration
|
[Reading 24] [Reading 25] [Reading 26] Homework 3 Due: by 11:59pm |
Lecture 22 | 4/16 |
Concept: Formal methods in the real world
|
|
Lecture 23 | 4/18 |
Concepts: Angelic Execution
|
|
Lecture 24 | 4/23 |
Concepts: Program Synthesis for Java
|
[Reading 27] [Reading 28] |
Lecture 25 | 4/25 |
Concepts: Solver-Aided Languages
|
[Reading 29] [Reading 30] |
Lecture 26 | 4/30 |
No class: Project work day
|
Presentation Slides Due: by 11:59pm |
Lecture 27 | 5/2 | Concepts: Final Project Presentations | |
5/6 | Final Project Turn-In: Project report and source code due by 11:59 pm |