Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
cs-486:schedule [2020/01/13 12:44]
egm
cs-486:schedule [2020/01/21 16:37]
egm
Line 4: Line 4:
 ^ Week ^ Topic and Reading ^ Due ^ ^ Week ^ Topic and Reading ^ Due ^
 | Week 1 | Course overview, and finding bugs in concurrent systems ​ | |  | Week 1 | Course overview, and finding bugs in concurrent systems ​ | | 
-|        | Overview of PROMELA and SPIN | [[Homework 0]]|+|        | 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]) | | | 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 | [[Homework 1]] | +|        | 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]) |  | | 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 | [[Homework 2]] |+|        | 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])  | | | 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 ​ |[[Homework 3]]|+|        | 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])  |  | | 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]]|+|        | 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) | | | 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]] |+|        | 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])| ​ | | 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]]  |  +|        | 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 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 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 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 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)  |  |  | 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 10 | Homework 11]] |+|         | If-then-else ITE) for ROBDDs ([[Lectures | ITE.ppt]]) | Homework 11 |
 | Week 13 | SwapVariables Algorithm for ROBDDs ([[Lectures | Replace.ppt]]) | | | Week 13 | SwapVariables Algorithm for ROBDDs ([[Lectures | Replace.ppt]]) | |
 |         | AndAbstract for ROBDDs--natural join ([[Lectures | RelProd.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 13 | Homework 12]] |+| 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) |  | |         | 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 15 | Review and Course Wrap-up | | 
 | Week 16 | Finals | [[Exams | Final]] | | Week 16 | Finals | [[Exams | Final]] |
  
cs-486/schedule.txt · Last modified: 2020/01/21 16:37 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