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
Last revision Both sides next revision
cs-486:schedule [2018/12/11 14:52]
egm
cs-486:schedule [2020/01/17 17:34]
egm
Line 1: Line 1:
-The official schedule for the semester is found on [http://​learningsuite.byu.edu BYU Learning Suite]. Here is the general template.  ​+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 ^ 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 ​ | 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