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 Forskningsparken  Model Checking - Foundations  Automata & Logic (Holzmann Chap. 6)

Slides 

11.03.2009Cristian Prisacariu  room 41151 Forskningsparken  Foundations, Promela  LTL into Automata (Peled Chap. 6)

Overview of Promela (Holzmann Chap. 2 & 3)

Slides 

18.03.2009Cristian Prisacariu  room 41151 Forskningsparken  Promela  Promela Semantics (Holzmann Chap. 7)

Slides 

25.03.2009Cristian Prisacariu  room 41151 Forskningsparken  Promela  Correctness claims (Holzmann Chap. 4)

Slides 

01.04.2009Cristian Prisacariu  room 41151 Forskningsparken  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 Forskningsparken  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 Forskningsparken  Mandatory Assignment + Presentation Drafts  All students must show the drafts of their respective presentations. 
29.04.2009E. & C. & G.  room 41151 Forskningsparken  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 Forskningsparken  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 Forskningsparken   Great debates   
20.05.2009E. & C. & G.  room 41151 Forskningsparken  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