INF5140 - V?r 2009

Undervisningsplan

DatoUndervises avStedTemaKommentarer / ressurser
21.01.2009Gerardo Schneider? 3B? Introduction? Slides ?
28.01.2009Espen H. Lian? 3B? First order logic, SPL syntax, Hoare logic? Slides ?
04.02.2009Espen H. Lian? 3B? Fair transition systems, SPL semantics? Slides?
11.02.2009Espen H. Lian? 3B? Linear temporal logic? Slides?
18.02.2009Espen H. Lian? 3B? Proof methods? Slides?
25.02.2009Espen H. Lian? 3B? Branching-time logics, modal logic? Slides?
04.03.2009Cristian Prisacariu? room 41151 澳门葡京手机版app下载sparken? Model Checking - Foundations? Automata & Logic (Holzmann Chap. 6)

Slides?

11.03.2009Cristian Prisacariu? room 41151 澳门葡京手机版app下载sparken? Foundations, Promela? LTL into Automata (Peled Chap. 6)

Overview of Promela (Holzmann Chap. 2 & 3)

Slides?

18.03.2009Cristian Prisacariu? room 41151 澳门葡京手机版app下载sparken? Promela? Promela Semantics (Holzmann Chap. 7)

Slides?

25.03.2009Cristian Prisacariu? room 41151 澳门葡京手机版app下载sparken? Promela? Correctness claims (Holzmann Chap. 4)

Slides?

01.04.2009Cristian Prisacariu? room 41151 澳门葡京手机版app下载sparken? Model Checking - SPIN? Part 0: Slides

Part 1 (Algorithms-Safety, Holzmann Chap. 8): See Holzmann's Slides (s. 8-22)

Part 2 (Algorithms-Liveness+Fairness, Holzmann Chap. 8): See Holzmann's Slides

Part 3 (Algorithms-P.O.R., Holzmann Chap. 9): See Holzmann's Slides (s. 1-14) ?

08.04.2009? ? EASTER? ?
15.04.2009Catalin Dima? room 41151 澳门葡京手机版app下载sparken? Model checking and satisfiability of an epistemic logic? We show that CTL with knowledge modalities but without common knowledge has an undecidable satisfiability problem in the synchronous perfect recall semantics. This result is in contrast with the case of LTL with knowledge, which has been shown by Halpern & Vardi (back in the 80s) to have a decidable satisfiability pro?
22.04.2009Cristian Prisacariu? room 41151 澳门葡京手机版app下载sparken? Mandatory Assignment + Presentation Drafts? All students must show the drafts of their respective presentations.?
29.04.2009E. & C. & G.? room 41151 澳门葡京手机版app下载sparken? Paper Presentation (madness day)? Mai: "State-of-the-art in Bounded Model Checking (SAT-based)" Paper

Abigail: "Model Checking by Bisimulation Equivalences" Book,chp.7

Fadli: "HyTech: A Model Checker for Hybrid Systems" Paper?

06.05.2009E. & C. & G.? room 41151 澳门葡京手机版app下载sparken? Paper Presentation (time-aware day)? Daniela: "Symbolic Model Checking (CTL) Paper

Fatemeh: "Theory of Timed Automata" Paper

Lizeth: "Model Checking Timed CTL" Paper?

13.05.2009Gerardo Schneider? room 41151 澳门葡京手机版app下载sparken ? Great debates? ?
20.05.2009E. & C. & G.? room 41151 澳门葡京手机版app下载sparken? Mandatory Assignment? Delivery - working code + Technical report describing: the problem (i.e. the system you modeled), the properties to check, results for each property and possible corrections improvements to the model you made, and also it has to show your way of working with the SPIN tool and helper tools it offers.?
27.05.2009? ? ? ?
Publisert 12. jan. 2009 12:40 - Sist endret 27. jan. 2011 19:47
Del p? e-post