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
cs-486/schedule.txt · Last modified: 2020/01/21 16:37 by egm
Back to top
CC Attribution-Share Alike 4.0 International = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0