The official schedule for the semester is found on BYU Learning Suite. Here is the general template.

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.5)
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) Homework 12
Week 14 CountMinterm ro ROBDD–how many items are in a set ( SatCount.ppt) Homework 13
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: 2017/09/26 16:00 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = 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