CS195Y
Spring '16
Brown's
Logic for
Systems

Course Materials

Note: readings from Software Abstractions (2nd edition) by Daniel Jackson (MIT Press) unless otherwise noted.

Date Lecture Notes (with Source Files) Reading
1/27 What is Logic for Systems?
1/29 Testing Oracles
2/1 Oracles and Properties (sort, tic tac toe)
2/3 Intro to Modeling in Alloy (tic tac toe) Ch. 2 (pg. 5-32)
2/5 Relational Expressions (tic tac toe)
2/8 Relational Expressions and Dynamics (Snow Day)
2/10 Multiplicities and Quantification (tic tac toe) Alloy Seq Documentation, Ch. 3 (33-83)
2/12 Modules, Numerics, and Events (courses)
2/15 Events (courses, data) Sec. 4.1-4.2 (pg. 85-103)
2/17 River Crossing Dynamics Sec. 4.4-4.8 (pg. 141-169)
2/19 Isomorphism, Symmetry, and Transitive Closure (symmetry breaking)
2/24 Transitive Closure Continued Ch. 5 (pg. 141-169)
2/26 Skolemization & Analysis Pitfalls (cities)
2/29 Modeling: Data Structures (trees)
3/2 Induction and Modeling
3/4 Induction and Modeling (trees)
3/7 Alloy Under the Hood
3/9 SAT Solving
3/11 SMT
4/4 Model Checking: Traffic Light in Alloy
4/6 Model Checking: Traffic Light in Spin
4/8 Model Checking: Locks (lock0, lock1, lock2)
4/11 Model Checking: Locks
4/13 Model Checking: Traffic Light
4/15 Spin Macros
4/18 Intro to (Liquid) Haskell Haskell Guide
4/20 Refinements in Liquid Haskell (refinements)
4/22 More Liquid Haskell Refinements
4/25 Natural Deduction
4/27 More Natural Deduction
4/29 Datalog
5/4 Decidability