2 Schedule
The course schedule is shown below. Slides will be posted after each lecture. Additional readings will be posted as well. If multiple references are listed for a lecture, you are only expected to read the first one. The rest are optional.
Final project demos will be held on Dec 08, 10:30am-12:20pm, in MGH 254.
Please fill out the course evaluation form. The evaluation opens on Dec 02 and closes on Dec 08.
Date |
| Topic |
| Slides |
| Reading |
| Assigned |
| Due |
09/25 |
| Introduction |
|
|
|
| ||||
09/30 |
| A Basic SAT Solver |
|
| [5] |
|
| |||
10/02 |
| A Modern SAT Solver |
|
|
|
| ||||
10/07 |
| Applications of SAT |
|
| [23] |
|
| |||
10/09 |
| SAT Modulo Theories |
|
| [20] |
|
| |||
10/14 |
| A Survey of Theory Solvers |
|
| [6] |
|
| |||
10/16 |
| Combining Theories |
|
| [4] |
|
| |||
10/21 |
| The DPPL(T) Framework |
|
| [3] |
|
| |||
10/23 |
| Finite Model Finding |
|
| [8] |
|
| |||
10/28 |
| Reasoning about Programs |
|
| [14] |
|
| |||
10/30 |
| Verification |
|
| [2] |
|
| |||
11/04 |
| Bounded Verification |
|
|
|
| ||||
11/06 |
| Symbolic Execution |
|
| [7] |
|
| |||
11/11 |
| Veteran’s Day, no class |
|
|
|
| ||||
11/13 |
| Model Checking I |
|
|
|
| ||||
11/18 |
| Model Checking II |
|
| [15] |
|
| |||
11/20 |
| Verifying Optimizations |
|
| [16] |
|
| |||
11/25 |
| Angelic Execution |
|
|
|
| ||||
11/27 |
| Thanksgiving, no class |
|
|
|
| ||||
12/02 |
| Program Synthesis |
|
| [22] |
|
| |||
12/04 |
| Solver-Aided Languages |
|
|
|
| ||||
12/08 |
|
|
|
|
|