search
All the due dates for homework and midterms are on BYU Learning Suite. Here is the W20 Schedule. Below is an outline that is generally followed.
| Week | Topic and Reading | Due |
|---|---|---|
| Week 1 | Course overview, and finding bugs in concurrent systems | |
| Overview of PROMELA and SPIN | Homework 0 | |
| Week 2 | PROMELA: Basic Data-types, processes, and control structures (Principles of the SPIN Model Checker Chapter 3) | |
| PROMELA: interleave, doran-thomas mutex, pnueli-mutex, mutex-unamed, dijkstras-simplification | Homework 1 | |
| Week 3 | PROMELA: Channels, pre-defined variables, labels, and end-states (Principles of the SPIN Model Checker Chapter 7) | |
| PROMELA: leader election, dining philosophers, and alternating bit | Homework 2 | |
| Week 4 | Safety versus liveness properties, NFAs for regular safety properties, and Intersecting NFAs (Principles of Model Checking Section 4.1 and 4.2) | |
| Kripke to NFA conversion, Never-claims in PROMELA, the German Traffic Light controller | Homework 3 | |
| Week 5 | SPIN Never-claims (Principles of the SPIN Model Checker Chapter 10) | |
| Buchi automaton and omega regular expressions (Model Checking Sections 9.1 - 9.2) | Homework 4 | |
| Week 6 | Intersecting Buchi Automaton (Model Checking Sections 9.3) | |
| Double-depth-first search, on-the-fly model checking, Non-progress cycles (Principles of the SPIN Model Checker Chapter 10.3) | Homework 5 | |
| Week 7 | SPIN Accept and Progress Labels (Principles of the SPIN Model Checker Chapter 10.3) | |
| Temporal Logic (Model Checking Chapter 3) | Homework 6 | |
| Week 8 | Temporal Logic (Model Checking Chapter 3) | Homework 7 |
| Week 9 | LTL Model Checking in SPIN (Principles of the SPIN Model Checker Chapter 5) | Homework 8 |
| Week 10 | CTL Model Checking (Model Checking Chapter 4) | Homework 9 |
| Week 11 | CTL Model Checking with Relational Algebra (Model Checking Sections 6.1) | Homework 10 |
| Week 12 | Reduced Ordered Binary Decision Diagrams (Model Checking Sections 6.1) | |
| If-then-else ITE) for ROBDDs ( ITE.ppt) | Homework 11 | |
| Week 13 | SwapVariables Algorithm for ROBDDs ( Replace.ppt) | |
| AndAbstract for ROBDDs–natural join ( RelProd.ppt) | ||
| Week 14 | CountMinterm ro ROBDD–how many items are in a set ( SatCount.ppt) | Homework 12 |
| CTL Model Checking with ROBDDs and CUDD ( ctl-sym-mc.ppt and Model Checking Sections 6.2 - 6.3) | ||
| Week 15 | Review and Course Wrap-up | |
| Week 16 | Finals | Final |
