| Date | Lecture Topic | Assignment Out | Assignment Due |
|---|---|---|---|
| Wed Feb 2 | Lightweight Formal Methods;
How to Avoid Lousy Software Please Fill out a background survey. Slides: intro and history Slides: software abstraction | Reading A: Introductory Flames | --- |
| Mon Feb 7 | Relational Logic | PS0: Relational Logic Exercises and Reading | Reading A
Sample Solutions |
| Wed Feb 9 | Alloy Language I,
Relational Logic Review Bring Laptop with Alloy installed (if able) | --- | --- |
| Mon Feb 14 | Alloy Language II | PS1: Simple Alloy Models | PS0 due
Sample Solutions |
| Wed Feb 16 | Introduction to Alloy as a Tool
file system: fs.als (DNJ away, lecture by Rob Seater) | --- | --- |
| Tue Feb 22 | TUESDAY
Case Study: Stateless Analysis of a Cryptographic Protocol (DNJ away, lecture by Emina Torlak) pdf slides | Reading B: Formal Methods and Software Design: Advocacy and Critique. | PS1
sample solutions: #1-3 #4 |
| Wed Feb 23 | Case Study: Radiotherapy Safety
(DNJ away, lecture by Greg Dennis) ppt slides pdf slides zipped models | --- | --- |
| Mon Feb 28 | Discussion: Formal Methods and Software Design: Advocacy and Critique. | PS2: Static Alloy Model | Reading B
sample solutions |
| Wed Mar 2 | Scope-Complete Analysis
TA's notes in PDF: 1 2 3 4 | --- | --- |
| Mon Mar 7 | Pattern: States and Operations
ring election: ringelection.als data ring updates: istate.als address book: bookdecl.als | --- | --- |
| Wed Mar 9 | Pattern: Declarative Modeling | Reading C: Z Specifications | PS2 |
| Mon Mar 14 | Pattern: Z Style
Modeling Patterns: incremental state, split operations, local state, trace and diameter | Reading D: Beyond Interfaces | Reading C |
| Wed Mar 16 | Lecture and Discussion: Beyond Interfaces | PS3: Dynamic Alloy Model | Reading D |
| Mon Mar 21 | SPRING BREAK no class | --- | --- |
| Wed Mar 23 | SPRING BREAK no class | --- | --- |
| Mon Mar 28 | Modal Logic (CTL*)
DNJ scanned notes TA's notes written notes by Ed Clarke: classic paper lecture slides (upside down) | --- | --- |
| Wed Mar 30 | Modal Logic (CTL vs. LTL)
DNJ scanned notes | --- | --- |
| Mon Apr 4 | Explicit State CTL Model Checking
DNJ scanned notes | --- | PS3 |
| Wed Apr 6 | Symbolic Model Checking
DNJ scanned notes Symbolic Model Checking, a paper by Biere et. al. | PS4: Modal Logic and Model Checking with NuSMV | --- |
| Mon Apr 11 | Hoare Logic
DNJ scanned notes | --- | --- |
| Wed Apr 13 | Code Verification Tools
DNJ scanned notes | PS5: Proving the Correctness of a Procedure | PS4 |
| Mon Apr 18 | HOLIDAY
no class | --- | --- |
| Wed Apr 20 | Refinement
Zip of Alloy model of abstraction relations DNJ scanned notes | FINAL PROJECT | PS5 |
| Mon Apr 25 | PASSOVER
no class | --- | --- |
| Wed Apr 27 | A Survey of Visual Notations
DNJ scanned notes | Reading E: The Nature of Bugs in Software. | Final Project Proposal |
| Mon May 2 | Dependencies and Dependences
DNJ notes (txt) | --- | --- |
| Wed May 4 | Discussion: The Nature of Bugs in Software | Final Project slide presentations due Friday at 5pm | Reading E |
| Mon May 9 | Student Presentations on Final Projects
Fill out an exit survey. | --- | Final Project presentation slides |
| Wed May 11 | Student Presentations on Final Projects | --- | Final Project written report |