**This is an old revision of the document!**

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 |