Schedule

Week 1: SAT: Foundations

Mar 30 – Apr 5

Lecture

Tuesday, Mar 31

• Practice: Solver demos: verify, debug, synthesize
• Theory: Propositional logic, normal forms, and DPLL
• Studio: Setup clinic, first exercises, and logistics

Bibliography

• Who Builds a House Without Drawing Blueprints?
• The Wooden Firehouse
• Worse is Better

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

Lecture

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

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

Lecture

Tuesday, Apr 14

• Practice: Beyond booleans, theories in action
• Theory: EUF and congruence closure
• Studio: Equality and theories in Z3

Bibliography

• How Amazon Web Services Uses Formal Methods

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 4: Solvers: Arithmetic, Arrays, and Bitvectors

Apr 20 – Apr 26

Lecture

Tuesday, Apr 21

• Practice: Four theory solvers, four engineering problems
• Theory: Inside LRA, LIA, bitvectors, and arrays
• Studio: Reading discussion

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 5: SMT: Foundations

Apr 27 – May 3

Lecture

Tuesday, Apr 28

• Practice: Why theories must cooperate: three acts on mixed-theory formulas
• Theory: First-order logic + Nelson-Oppen for convex theories
• Studio: FOL evaluator, mixed-theory predict-then-check, purification

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 6: SMT: Quantifiers and DPLL(T)

May 4 – May 10

Lecture

Tuesday, May 5

• Practice: ForAll on a queue library and pitfalls
• Theory: DPLL(T): offline, online, and Delayed Theory Combination
• Studio: Reading discussion: limits of formal methods

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 7: Verification: Symbolic Execution

May 11 – May 17

Lecture

Tuesday, May 12

• Practice: Building an SE engine and finding bugs
• Theory: Path conditions and the strongest postcondition
• Studio: Hand-tracing SE and revisiting bvudiv2

Bibliography

• Who Builds a House Without Drawing Blueprints?
• AI Will Make Formal Verification Mainstream
• The Coming Need for Formal Specification

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 8: Verification: Hoare Logic and WP

May 18 – May 24

Lecture

Tuesday, May 19

• Practice: Building a WP-based verifier
• Theory: WP rules, soundness, and the SP/WP duality
• Studio: AI and formal methods

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 9: Mini-Project: Milestone

May 25 – May 31

Lecture

Tuesday, May 26

• Practice: PEC: a solver-aided tool case study
• Theory: Three solver-aided paradigms
• Studio: Design-review clinic

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)