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: Applications | Coding Assignment 1: SAT Solving |
| 3 | Apr 13 | Theory Solvers | Reading Reflection 2 |
| 4 | Apr 20 | SMT: Foundations | Coding Assignment 2: Theory Solvers |
| 5 | Apr 27 | SMT: Modeling | 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
Lecture
- Practice: SAT-first launch: modeling demo, shock-and-awe apps, Python/Z3 + SMT-LIB visibility
- Theory: Logic foundations: syntax/semantics, CNF/Tseitin, resolution/unit propagation, DPLL
- Studio: Laptop setup clinic + guided mini-exercises + logistics
Due: Friday, April 3 at 5:00 PM | 50 points
Bibliography
Week 2: SAT: Applications
Apr 6 – Apr 12
Lecture
- 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
Week 3: Theory Solvers
Apr 13 – Apr 19
Lecture
- Practice: Theory-solvers bridge: congruence and equality demos
- Theory: Theory solver foundations: EUF, linear arithmetic, theory combination
- Studio: Guided practice / discussion
Due: Friday, April 17 at 5:00 PM | 50 points
Bibliography
Week 4: SMT: Foundations
Apr 20 – Apr 26
Lecture
- Practice: Theory-focused coding clinic
- Theory: DPLL(T) motivation and architecture, SMT theory combination
- Studio: Reading discussion
Coding Assignment 2: Theory Solvers
Due: Friday, April 24 at 5:00 PM | 150 points
Week 5: SMT: Modeling
Apr 27 – May 3
Lecture
- Practice: SMT modeling lab: counterexamples, incremental solving
- Theory: SMT architecture deep dive, theory combination detail
- Studio: Guided practice / discussion
Due: Friday, May 1 at 5:00 PM | 50 points
Week 6: SMT: Engineering
May 4 – May 10
Lecture
- Practice: SMT coding clinic: debugging workflows, solver sympathy
- Theory: Advanced SMT reasoning for practical workflows
- Studio: Reading discussion
Coding Assignment 3: SMT
Due: Friday, May 8 at 5:00 PM | 150 points
Week 7: Program Verification
May 11 – May 17
Lecture
- Practice: Program verification workflow demo: Hoare logic to tools
- Theory: Verification foundations: Hoare logic, weakest precondition, model checking
- Studio: Guided practice / discussion
Due: Friday, May 15 at 5:00 PM | 50 points
Bibliography
Week 8: Verification in Practice
May 18 – May 24
Lecture
- Practice: Verification/model-checking coding lab
- Theory: Connecting verification back to SAT/theory/SMT pipeline
- Studio: Mini-project framing, scoping, feasibility
Coding Assignment 4: Verification
Due: Friday, May 22 at 5:00 PM | 150 points
Week 9: Mini-Project: Milestone
May 25 – May 31
Lecture
- Practice: Mini-project milestone studio + TA feedback rounds
- Theory: Extension-topic sampler
- Studio: Design review and risk-check clinic
Mini-Project Milestone
Due: Friday, May 29 at 5:00 PM | 50 points
Week 10: Mini-Project: Final
Jun 1 – Jun 7
Lecture
- Practice: Mini-project integration studio, demo rehearsal
- Theory: Solver engineering and toolbelt transfer
- Studio: Selected student demos + course retrospective
Mini-Project Final
Due: Friday, June 5 at 5:00 PM | 150 points