All the due dates for homework and midterms are on [http://learningsuite.byu.edu BYU Learning Suite]. 
Here is the [https://docs.google.com/spreadsheets/d/1LhWv9bcBmysMEbak7ahzvAWQBRAXC1hnM3uuPFrsNm8/edit?usp=sharing 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 | [https://bitbucket.org/byucs486/byu-cs-486-homework/src/master/hw0-spin-processes.md Homework 0]|
| Week 2 | PROMELA: Basic Data-types, processes, and control structures (Principles of the SPIN Model Checker [http://link.springer.com/chapter/10.1007/978-1-84628-770-1_3 Chapter 3]) | |
|        | PROMELA: interleave, doran-thomas mutex, pnueli-mutex, mutex-unamed, dijkstras-simplification | [https://bitbucket.org/byucs486/byu-cs-486-homework/src/master/hw1-mutual-exclusion-search.md Homework 1] | 
| Week 3 | PROMELA: Channels, pre-defined variables, labels, and end-states (Principles of the SPIN Model Checker [http://link.springer.com/chapter/10.1007/978-1-84628-770-1_3 Chapter 7]) |  |
|        | PROMELA: leader election, dining philosophers, and alternating bit | [https://bitbucket.org/byucs486/byu-cs-486-homework/src/master/hw2-nway-mutex-message-passing.md Homework 2] |
| Week 4 | Safety versus liveness properties, NFAs for regular safety properties, and Intersecting NFAs ([http://is.ifmo.ru/books/_principles_of_model_checking.pdf Principles of Model Checking Section 4.1 and 4.2])  | |
|        | Kripke to NFA conversion, Never-claims in PROMELA, the German Traffic Light controller  | [https://bitbucket.org/byucs486/byu-cs-486-homework/src/master/hw3-dijkstras-token-termination.md Homework 3]|
| Week 5 | SPIN Never-claims (Principles of the SPIN Model Checker [http://link.springer.com/chapter/10.1007/978-1-84628-770-1_3 Chapter 10])  |  |
|        | Buchi automaton and omega regular expressions ([http://web.b.ebscohost.com/ehost/detail/detail?vid=0&sid=3203e77a-2a69-48e8-a137-343d241cf23e%40sessionmgr101&bdata=JnNpdGU9ZWhvc3QtbGl2ZSZzY29wZT1zaXRl#AN=27235&db=nlebk Model Checking] Sections 9.1 - 9.2) | Homework 4|
 
| Week 6 | Intersecting Buchi Automaton ([http://web.b.ebscohost.com/ehost/detail/detail?vid=0&sid=3203e77a-2a69-48e8-a137-343d241cf23e%40sessionmgr101&bdata=JnNpdGU9ZWhvc3QtbGl2ZSZzY29wZT1zaXRl#AN=27235&db=nlebk Model Checking] Sections 9.3) | |
|        | Double-depth-first search, on-the-fly model checking, Non-progress cycles (Principles of the SPIN Model Checker [http://link.springer.com/chapter/10.1007/978-1-84628-770-1_3 Chapter 10.3])  |Homework 5 |
| Week 7 | SPIN Accept and Progress Labels (Principles of the SPIN Model Checker [http://link.springer.com/chapter/10.1007/978-1-84628-770-1_3 Chapter 10.3])|  |
|        | Temporal Logic ([http://web.b.ebscohost.com/ehost/detail/detail?vid=0&sid=3203e77a-2a69-48e8-a137-343d241cf23e%40sessionmgr101&bdata=JnNpdGU9ZWhvc3QtbGl2ZSZzY29wZT1zaXRl#AN=27235&db=nlebk Model Checking] Chapter 3)  | Homework 6  | 
| Week 8 | Temporal Logic ([http://web.b.ebscohost.com/ehost/detail/detail?vid=0&sid=3203e77a-2a69-48e8-a137-343d241cf23e%40sessionmgr101&bdata=JnNpdGU9ZWhvc3QtbGl2ZSZzY29wZT1zaXRl#AN=27235&db=nlebk Model Checking] Chapter 3) | Homework 7  | 
| Week 9 | LTL Model Checking in SPIN (Principles of the SPIN Model Checker [http://link.springer.com/chapter/10.1007/978-1-84628-770-1_3 Chapter 5]) | Homework 8|
| Week 10 | CTL Model Checking ([http://web.b.ebscohost.com/ehost/detail/detail?vid=0&sid=3203e77a-2a69-48e8-a137-343d241cf23e%40sessionmgr101&bdata=JnNpdGU9ZWhvc3QtbGl2ZSZzY29wZT1zaXRl#AN=27235&db=nlebk Model Checking] Chapter 4)  | Homework 9 |
| Week 11 | CTL Model Checking with Relational Algebra ([http://web.b.ebscohost.com/ehost/detail/detail?vid=0&sid=3203e77a-2a69-48e8-a137-343d241cf23e%40sessionmgr101&bdata=JnNpdGU9ZWhvc3QtbGl2ZSZzY29wZT1zaXRl#AN=27235&db=nlebk Model Checking] Sections 6.1) | Homework 10  |
| Week 12 | Reduced Ordered Binary Decision Diagrams ([http://web.b.ebscohost.com/ehost/detail/detail?vid=0&sid=3203e77a-2a69-48e8-a137-343d241cf23e%40sessionmgr101&bdata=JnNpdGU9ZWhvc3QtbGl2ZSZzY29wZT1zaXRl#AN=27235&db=nlebk Model Checking] Sections 6.1)  |  | 
|         | If-then-else ITE) for ROBDDs ([[Lectures | ITE.ppt]]) | Homework 11 |
| Week 13 | SwapVariables Algorithm for ROBDDs ([[Lectures | Replace.ppt]]) | |
|         | AndAbstract for ROBDDs--natural join ([[Lectures | RelProd.ppt]])| | 
| Week 14 | CountMinterm ro ROBDD--how many items are in a set ([[Lectures | SatCount.ppt]]) | Homework 12 |
|         | CTL Model Checking with ROBDDs and CUDD ([[Lectures | ctl-sym-mc.ppt]] and [http://web.b.ebscohost.com/ehost/detail/detail?vid=0&sid=3203e77a-2a69-48e8-a137-343d241cf23e%40sessionmgr101&bdata=JnNpdGU9ZWhvc3QtbGl2ZSZzY29wZT1zaXRl#AN=27235&db=nlebk Model Checking] Sections 6.2 - 6.3) |  |
| Week 15 | Review and Course Wrap-up | | 
| Week 16 | Finals | [[Exams | Final]] |