This shows you the differences between two versions of the page.
courses:av2009:main [2009/04/10 01:23] tsay |
courses:av2009:main [2009/06/24 11:32] (current) tsay |
||
---|---|---|---|
Line 4: | Line 4: | ||
===== Announcements ===== | ===== Announcements ===== | ||
- | * 2/24: slides for Introduction and Systems Modeling available | + | * 6/23: belated slides for Automata-Theoretic Approach available |
- | * 3/9: slides for Temporal Logic Model Checking available | + | * 6/22: slides for Compositional Reasoning and Infinite-State Systems available |
- | * 3/18: slides for Ordered Sets and BDDs available | + | * 5/23: slides for Bounded Model Checking available |
- | * 3/19: slides for BDDs revised | + | * 5/19: slides for Equivalences and Abstraction and for SAT Solving available |
+ | * 5/18: {{courses:av2009:hw1.pdf|Homework Assignment #1}} and {{courses:av2009:hw2.pdf|Homework Assignment #2}} due May 27 | ||
+ | * 5/18: slides for Symbolic Model Checkers and the SPIN Model Checker available | ||
+ | * 4/20: slides for mu-Calculus available | ||
* 4/9: slides for Symbolic Model Checking available | * 4/9: slides for Symbolic Model Checking available | ||
+ | * 3/19: slides for BDDs revised | ||
+ | * 3/18: slides for Ordered Sets and BDDs available | ||
+ | * 3/9: slides for Temporal Logic Model Checking available | ||
+ | * 2/24: slides for Introduction and Systems Modeling available | ||
===== Instructor ===== | ===== Instructor ===== | ||
Line 40: | Line 47: | ||
* Binary Decision Diagrams [CGP: Ch. 5; SP] (1 week: 3/18) [{{courses:av2009:bdd.pdf|slides}}] | * Binary Decision Diagrams [CGP: Ch. 5; SP] (1 week: 3/18) [{{courses:av2009:bdd.pdf|slides}}] | ||
* Symbolic Model Checking [CGP: Ch. 6] (1 week: 3/25) [{{courses:av2009:symbolic_model_checking.pdf|slides}}] | * Symbolic Model Checking [CGP: Ch. 6] (1 week: 3/25) [{{courses:av2009:symbolic_model_checking.pdf|slides}}] | ||
- | * Model Checking μ-Calculus [CGP: Ch. 7] (1 week: 4/1) | + | * Model Checking μ-Calculus [CGP: Ch. 7] (1 week: 4/1) [{{courses:av2009:mu_calculus.pdf|slides}}] |
- | * Symbolic Model Checkers [CGP: Ch. 8; SP; CN] (1 week: 4/8) | + | * Symbolic Model Checkers [CGP: Ch. 8; SP; CN] (1 week: 4/8) [{{courses:av2009:symbolic_model_checkers.pdf|slides}}] |
- | * Automata-Theoretic Approach [CGP: Ch. 9; BK: Ch. 4.3,4.4,5; H: Ch. 6; MP: Ch. 5.1] (1 week: 4/15) | + | * Automata-Theoretic Approach [CGP: Ch. 9; BK: Ch. 4.3,4.4,5; H: Ch. 6; MP: Ch. 5.1] (1 week: 4/15) [{{courses:av2009:automata_theoretic_approach.pdf|slides}}] |
- | * The Spin Model Checker [H: Ch. 3, 4, 7, 12] (1 week: 4/22) | + | * The Spin Model Checker [H: Ch. 3, 4, 7, 12] (1 week: 4/22) [{{courses:av2009:the_spin_model_checker.pdf|slides}}] |
- | * Partial Order Reduction [CGP: Ch. 10; BK: Ch. 8] (1 week: 4/29) | + | * Partial Order Reduction [CGP: Ch. 10; BK: Ch. 8] (1 week: 4/29) (cancelled to leave time for other topics) |
- | * Equivalences and Abstraction [CGP: Ch. 11,13; BK: Ch. 7; SP] (1 week: 5/6) | + | * Equivalences and Abstraction [CGP: Ch. 11,13; BK: Ch. 7; SP] (1 week: 5/6) [{{courses:av2009:abstraction.pdf|slides}}] |
- | * Satisfiability Solving and Tools [SP; CN] (1 week: 5/13) | + | * Satisfiability Solving and Tools [SP; CN] (1 week: 5/13) [{{courses:av2009:sat.pdf|slides}}] |
- | * Bounded Model Checking [SP] (1 week: 5/20) | + | * Bounded Model Checking [SP] (1 week: 5/20) [{{courses:av2009:bounded_model_checking.pdf|slides}}] |
* **Final** (**2009/05/27**) | * **Final** (**2009/05/27**) | ||
* Satisfiability Modulo Theories (SMT), Solvers, and Applications [SP; CN] (1 week: 6/3) | * Satisfiability Modulo Theories (SMT), Solvers, and Applications [SP; CN] (1 week: 6/3) | ||
- | * Compositional Reasoning [CGP: Ch. 12; SP; CN] (1 week: 6/10) | + | * Compositional Reasoning [CGP: Ch. 12; SP; CN] (1 week: 6/10) [{{courses:av2009:compositional_reasoning.pdf|slides}}] |
- | * Infinite-State Systems [CGP: Ch. 15; SP] (1 week: 6/17) | + | * Infinite-State Systems [CGP: Ch. 15; SP] (1 week: 6/17) [{{courses:av2009:infinite_systems.pdf|slides}}] |
===== Grading ===== | ===== Grading ===== |