search
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
cs-486:schedule [2020/01/17 17:34] egm |
cs-486:schedule [2020/01/21 16:37] (current) egm |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| | | 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] | | | | 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| | ||
