User Tools
courses:av2011:main
Differences
This shows you the differences between two versions of the page.
|
courses:av2011:main [2011/02/18 18:47] tsay created |
courses:av2011:main [2011/06/02 22:39] (current) tsay |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| ===== Announcements ===== | ===== Announcements ===== | ||
| + | * 06/02: {{courses:av2011:hw4.pdf|HW#4}} due on 06/09. | ||
| + | * 06/02: slides for Abstraction and Compositional Reasoning available. | ||
| + | * 05/19: slides for Symbolic Model Checkers and the Spin Model Checker available. | ||
| + | * 05/19: {{courses:av2011:hw3.pdf|HW#3}} due on 05/26. | ||
| + | * 05/14: slides for Binary Decision Diagrams revised (changes only made on the Reduction example). | ||
| + | * 05/14: slides for Symbolic Model Checking and for Model Checking Mu-Calculus available. | ||
| + | * 05/12: slides for Automata-Theoretic Approach available (slightly improved over the version distributed in class). | ||
| + | * 05/12: {{courses:av2011:hw2.pdf|HW#2}} was due. | ||
| + | * 04/14: slides for Binary Decision Diagrams available. | ||
| + | * 03/25: {{courses:av2011:hw1.pdf|HW#1}} due on 04/14. | ||
| + | * 03/17: slides for Temporal Logic Model Checking and Ordered Sets and Fixpoints available. | ||
| + | * 02/24: slides for Introduction and Systems Modeling available. | ||
| ===== Instructor ===== | ===== Instructor ===== | ||
| - | Yih-Kuen Tsay (蔡益坤), NTU IM Dept., 3366-1189, ''Xtsay@im.ntu.edu.twX'' (between the enclosing pair of X's) | + | Yih-Kuen Tsay (蔡益坤), NTU IM Dept., 3366-1189, ''http://im.ntu.edu.tw/~tsay/'', ''Xtsay@im.ntu.edu.twX'' (between the enclosing pair of X's) |
| ===== Lectures ===== | ===== Lectures ===== | ||
| - | Wednesday 9:10AM-12:10PM, Room 203, Management II (when the class is small enough, we meet in the seminar room on the 11th floor) | + | Thursday 2:20PM-5:20PM, Room 204, Management II (when the class is small enough, we meet in the seminar room on the 11th floor) |
| ===== Office Hours ===== | ===== Office Hours ===== | ||
| Line 33: | Line 45: | ||
| * Introduction [CGP: Ch. 1; BK: Ch. 1; H: Ch. 1] (.5 week: 2/24a) [{{courses:av2011:introduction.pdf|slides}}] | * Introduction [CGP: Ch. 1; BK: Ch. 1; H: Ch. 1] (.5 week: 2/24a) [{{courses:av2011:introduction.pdf|slides}}] | ||
| * Systems Modeling [CGP: Ch. 2; BK: Ch. 2,3; H: Ch. 2; MP: Ch. 0.1-4] (.5 week: 2/24b) [{{courses:av2011:modeling.pdf|slides}}] | * Systems Modeling [CGP: Ch. 2; BK: Ch. 2,3; H: Ch. 2; MP: Ch. 0.1-4] (.5 week: 2/24b) [{{courses:av2011:modeling.pdf|slides}}] | ||
| - | * Temporal Logic Model Checking [CGP: Ch. 3,4; BK: Ch. 6; MP: Ch. 5.2-3] (2 weeks: 3/3, 3/10) [{{courses:av2011:temporal_logic_model_checking.pdf|slides}}] | + | * Temporal Logic Model Checking [CGP: Ch. 3,4; BK: Ch. 6; MP: Ch. 5.2-3] (2 weeks: 3/3, 3/5) [{{courses:av2011:temporal_logic_model_checking.pdf|slides}}] |
| - | * Ordered Sets and Fixpoints [CN] (1 week: 3/17) [{{courses:av2011:ordered_sets.pdf|slides}}] | + | * Ordered Sets and Fixpoints [CN] (1.5 weeks: 3/10, 3/17a) [{{courses:av2011:ordered_sets.pdf|slides}}] |
| - | * Binary Decision Diagrams [CGP: Ch. 5; SP] (1 week: 3/24) [{{courses:av2011:bdd.pdf|slides}}] | + | * Binary Decision Diagrams [CGP: Ch. 5; SP] (1.5 weeks: 3/17b, 3/24) [{{courses:av2011:bdd.pdf|slides}}] |
| - | * Symbolic Model Checking [CGP: Ch. 6] (1 week: 3/31) [{{courses:av2011:symbolic_model_checking.pdf|slides}}] | + | * Symbolic Model Checking [CGP: Ch. 6] (2 weeks: 4/9, 4/14) [{{courses:av2011:symbolic_model_checking.pdf|slides}}] |
| - | * Model Checking μ-Calculus [CGP: Ch. 7] (1 week: 4/14) [{{courses:av2011:mu_calculus.pdf|slides}}] | + | * Model Checking μ-Calculus [CGP: Ch. 7] (1 week: 4/21) [{{courses:av2011:mu_calculus.pdf|slides}}] |
| - | * Symbolic Model Checkers [CGP: Ch. 8; SP; CN] (1 week: 4/21) [{{courses:av2011:symbolic_model_checkers.pdf|slides}}; [{{courses:av2011:nusmv_cmd.pdf|note}}] | + | * Symbolic Model Checkers [CGP: Ch. 8; SP; CN] (1 week: 4/28) [{{courses:av2011: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/28) [{{courses:av2011: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: 5/5) [{{courses:av2011:automata_theoretic_approach.pdf|slides}}] |
| - | * The Spin Model Checker [H: Ch. 3, 4, 7, 12] (1 week: 5/5) [{{courses:av2011:the_spin_model_checker.pdf|slides}}] | + | * The Spin Model Checker [H: Ch. 3, 4, 7, 12] (1 week: 5/12) [{{courses:av2011:the_spin_model_checker.pdf|slides}}] |
| - | * Equivalences and Abstraction [CGP: Ch. 11,13; BK: Ch. 7; SP] (1 week: 5/12) [{{courses:av2011:abstraction.pdf|slides}}] | + | * Equivalences and Abstraction [CGP: Ch. 11,13; BK: Ch. 7; SP] (1 week: 5/19) [{{courses:av2011:abstraction.pdf|slides}}] |
| - | * Compositional Reasoning [CGP: Ch. 12; SP; CN] (1 week: 5/19) [{{courses:av2011:compositional_reasoning.pdf|slides}}] | + | * Compositional Reasoning [CGP: Ch. 12; SP; CN] (1 week: 5/26) [{{courses:av2011:compositional_reasoning.pdf|slides}}] |
| - | * Satisfiability Solving and Tools [SP; CN] (1 week: 5/26) [{{courses:av2011:sat.pdf|slides}}] | + | * Satisfiability Solving and Tools [SP; CN] (1 week: 6/2) [{{courses:av2011:sat.pdf|slides}}] |
| - | * Bounded Model Checking [SP] (1 week: 6/2) [{{courses:av2011:bounded_model_checking.pdf|slides}}] | + | * Bounded Model Checking [SP] (1 week: 6/9) [{{courses:av2011:bounded_model_checking.pdf|slides}}] |
| - | * **Final** (**2010/06/09**) | + | * **Final** (**2011/06/16**) |
| * Satisfiability Modulo Theories (SMT), Solvers, and Applications [SP; CN] (1 week: 6/23) [{{courses:av2011:smt.pdf|slides}}] | * Satisfiability Modulo Theories (SMT), Solvers, and Applications [SP; CN] (1 week: 6/23) [{{courses:av2011:smt.pdf|slides}}] | ||
| ===== Grading ===== | ===== Grading ===== | ||
| - | Homework Assignments 20%, Final Exam 40%, Term Paper/Report 40%. | + | Homework Assignments 20%, Participation 10%, Final Exam 40%, Term Paper/Report 30%. |
courses/av2011/main.1298026072.txt.gz · Last modified: 2011/02/18 18:47 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
