Schedule
CARS runs on a predictable weekly rhythm. Lecture meets every
Tuesday evening. One deliverable is due every Friday at 5:00 PM.
Odd weeks have a reading reflection; even weeks have a coding
assignment. The last two weeks are for the mini-project. Each
lecture covers what you need for that week's work, so everything
stays self-contained.
| # | Week | Topic | Deliverable |
| 1 | Mar 30 | SAT: Foundations | Reading Reflection 1 |
| 2 | Apr 6 | SAT: Solving and Applications | Coding Assignment 1: SAT Solving |
| 3 | Apr 13 | Solvers: Theories and Equality | Reading Reflection 2 |
| 4 | Apr 20 | Solvers: Arithmetic, Arrays, and Bitvectors | Coding Assignment 2: Theory Solvers |
| 5 | Apr 27 | SMT: Foundations | Reading Reflection 3 |
| 6 | May 4 | SMT: Engineering | Coding Assignment 3: SMT |
| 7 | May 11 | Program Verification | Reading Reflection 4 |
| 8 | May 18 | Verification in Practice | Coding Assignment 4: Verification |
| 9 | May 25 | Mini-Project: Milestone | Mini-Project Milestone |
| 10 | Jun 1 | Mini-Project: Final | Mini-Project Final |
Week 1: SAT: Foundations
Mar 30 – Apr 5
Tuesday, Mar 31
- Practice: Solver demos: verify, debug, synthesize
- Theory: Propositional logic, normal forms, and DPLL
- Studio: Setup clinic, first exercises, and logistics
Due: Friday, April 3 at 5:00 PM | 50 points
Bibliography
Office Hours
- Tue 5:30-6:30 PM, CSE2 201 (Zachary Tatlock)
- Thu 5:30-6:30 PM, Zoom (Glenn Sun)
- Sat 5:30-6:30 PM, Zoom (Audrey Seo)
Week 2: SAT: Solving and Applications
Apr 6 – Apr 12
Tuesday, Apr 7
- Practice: Larger SAT apps: encoding quality, scalability, solver sympathy
- Theory: CDCL deep dive: conflict analysis, non-chronological backtracking, solver behavior intuition
- Studio: Reading discussion
Coding Assignment 1: SAT Solving
Due: Friday, April 10 at 5:00 PM | 150 points
Office Hours
- Tue 5:30-6:30 PM, CSE2 201 (Zachary Tatlock)
- Thu 5:30-6:30 PM, Zoom (Audrey Seo)
- Sat 5:30-6:30 PM, Zoom (Glenn Sun)
Week 3: Solvers: Theories and Equality
Apr 13 – Apr 19
Tuesday, Apr 14
- Practice: Beyond booleans, theories in action
- Theory: EUF and congruence closure
- Studio: Equality and theories in Z3
Due: Friday, April 17 at 5:00 PM | 50 points
Bibliography
Office Hours
- Tue 5:30-6:30 PM, CSE2 201 (Zachary Tatlock)
- Thu 5:30-6:30 PM, Zoom (Glenn Sun)
- Sat 5:30-6:30 PM, Zoom (Audrey Seo)