This shows you the differences between two versions of the page.
courses:av2010:main [2010/03/24 12:35] tsay |
courses:av2010:main [2010/06/03 08:25] (current) tsay |
||
---|---|---|---|
Line 3: | Line 3: | ||
===== Announcements ===== | ===== Announcements ===== | ||
+ | * 6/03: slides for SAT Solving and Tools available | ||
+ | * 5/26: slides for Compositional Reasoning available | ||
+ | * 5/26: {{courses:av2010:hw2.pdf|HW#2}} due on June 9 | ||
+ | * 5/19: slides for Equivalences and Abstraction available | ||
+ | * 5/19: slides for SPIN available | ||
+ | * 5/18: slides and note for Symbolic Model Checkers available | ||
+ | * 4/28: slides for Automata-Theoretic Approach available | ||
+ | * 4/21: slides for Model Checking mu-Calculus available | ||
+ | * 4/13: {{courses:av2010:hw1.pdf|HW#1}} due on April 21 | ||
* 3/24: slides for Binary Decision Diagrams available | * 3/24: slides for Binary Decision Diagrams available | ||
* 3/20: slides for Ordered Sets and Fixpoints available | * 3/20: slides for Ordered Sets and Fixpoints available | ||
Line 39: | Line 48: | ||
* Symbolic Model Checking [CGP: Ch. 6] (1 week: 3/31) [{{courses:av2010:symbolic_model_checking.pdf|slides}}] | * Symbolic Model Checking [CGP: Ch. 6] (1 week: 3/31) [{{courses:av2010:symbolic_model_checking.pdf|slides}}] | ||
* Model Checking μ-Calculus [CGP: Ch. 7] (1 week: 4/14) [{{courses:av2010:mu_calculus.pdf|slides}}] | * Model Checking μ-Calculus [CGP: Ch. 7] (1 week: 4/14) [{{courses:av2010:mu_calculus.pdf|slides}}] | ||
- | * Symbolic Model Checkers [CGP: Ch. 8; SP; CN] (1 week: 4/21) [{{courses:av2010:symbolic_model_checkers.pdf|slides}}] | + | * Symbolic Model Checkers [CGP: Ch. 8; SP; CN] (1 week: 4/21) [{{courses:av2010:symbolic_model_checkers.pdf|slides}}; [{{courses:av2010:nusmv_cmd.pdf|note}}] |
* Automata-Theoretic Approach [CGP: Ch. 9; BK: Ch. 4.3,4.4,5; H: Ch. 6; MP: Ch. 5.1] (1 week: 4/28) [{{courses:av2010:automata_theoretic_approach.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/28) [{{courses:av2010:automata_theoretic_approach.pdf|slides}}] | ||
* The Spin Model Checker [H: Ch. 3, 4, 7, 12] (1 week: 5/5) [{{courses:av2010:the_spin_model_checker.pdf|slides}}] | * The Spin Model Checker [H: Ch. 3, 4, 7, 12] (1 week: 5/5) [{{courses:av2010:the_spin_model_checker.pdf|slides}}] | ||
Line 47: | Line 56: | ||
* Bounded Model Checking [SP] (1 week: 6/2) [{{courses:av2010:bounded_model_checking.pdf|slides}}] | * Bounded Model Checking [SP] (1 week: 6/2) [{{courses:av2010:bounded_model_checking.pdf|slides}}] | ||
* **Final** (**2010/06/09**) | * **Final** (**2010/06/09**) | ||
- | * Satisfiability Modulo Theories (SMT), Solvers, and Applications [SP; CN] (1 week: 6/23) | + | * Satisfiability Modulo Theories (SMT), Solvers, and Applications [SP; CN] (1 week: 6/23) [{{courses:av2010:smt.pdf|slides}}] |
===== Grading ===== | ===== Grading ===== |