User Tools
courses:av2010:main
Differences
This shows you the differences between two versions of the page.
|
courses:av2010:main [2010/02/19 20:27] tsay |
courses:av2010:main [2010/06/03 08:25] (current) tsay |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ===== Announcements ===== | ===== Announcements ===== | ||
| - | * 2/20: slides for Introduction and Systems Modeling available | + | * 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/20: slides for Ordered Sets and Fixpoints available | ||
| + | * 3/03: slides for Temporal Logic Model Checking available | ||
| + | * 2/24: {{courses:av2010:av2010info.pdf|PDF version}} of this page (as of 2010/02/24, without the announcements) | ||
| + | * 2/19: slides for Introduction and Systems Modeling available | ||
| ===== Instructor ===== | ===== Instructor ===== | ||
| - | Yih-Kuen Tsay (蔡益坤), Room 1108, Management II, 3366-1189, ''Xtsay@im.ntu.edu.twX'' (between the enclosing pair of X's) | + | Yih-Kuen Tsay (蔡益坤), NTU IM Dept., 3366-1189, ''Xtsay@im.ntu.edu.twX'' (between the enclosing pair of X's) |
| ===== Lectures ===== | ===== Lectures ===== | ||
| Line 35: | 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 43: | 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 ===== | ||
courses/av2010/main.1266582421.txt.gz · Last modified: 2010/02/19 20:27 by tsay
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 3.0 Unported
