Note: readings from Software Abstractions (2nd edition) by Daniel Jackson (MIT Press) unless otherwise noted.
| Date |
Lecture Notes (with Source Files) |
Reading |
| 1/25 |
What is Logic for Systems? |
|
| 1/27 |
Properties and Oracles |
|
| 1/30 |
Intro to Modeling in Alloy (tic tac toe 1) |
Ch. 2 (pg. 5-32) |
| 2/1 |
Relational Expressions (tic tac toe 2) |
|
| 2/3 |
Relational Expressions 2 |
|
| 2/6 |
Reachablity (cities) |
|
| 2/8 |
Multiplicities and Quantification (cities 2) |
|
| 2/10 |
Modules, Numerics, and Symmetry (cities 3) |
|
| 2/13 |
Skolemization and some Analysis Pitfalls (symmetry breaking, ints) |
|
| 2/15 |
More Skolemization and some Analysis Pitfalls (courses, skolem) |
|
| 2/17 |
Modeling Dynamic Systems (courses) |
|
| 2/22 |
More on Dynamics, Events (courses) |
|
| 2/24 |
Modeling Data Structures (courses) |
|
| 2/27 |
More on Data Structures, Induction (courses) |
|
| 3/1 |
Inductive Properties (descents, multitrees) |
|
| 3/3 |
Property-Free Analysis (addnode, descents) |
|
| 3/6 |
Inside Alloy |
|
| 3/8 |
SAT-Solving |
|
| 3/10 |
Resolution (propositional) |
|
| 3/13 |
Resolution (first-order) |
|
| 3/15 |
TBD |
|
| 3/17 |
More First Order Logic |
|
| 4/3 |
Introduction to Model Checking |
|
| 4/5 |
Model Checking (1) |
|
| 4/7 |
Model Checking (2)
[lock1, lock2, peterson] |
|
| 4/10 |
Model Checking (3) [light2.pml, nd.pml] |
|
| 4/12 |
Model Checking (4) [queuelock_soln.pml] |
|
| 4/14 |
Spin Internals |
|
| 4/17 |
Rosette (1) (0417-class.rkt) |
|
| 4/19 |
Rosette (2) |
|
| 4/21 |
SMT (1) (0421-class.rkt) |
|
| 4/24 |
SMT (2) |
|
| 4/26 |
SMT (3) |
|
| 4/28 |
Decidability |
|