Undervisningsplan

DatoUndervises avStedTemaKommentarer / ressurser
24.01.2007Gerardo Schneider  3B  Introduction  General remarks Slides

Introduction to formal methods Slides 

31.01.2007Espen H. Lian  3B  First Order Logic, SPL syntax, Hoare Logic  Slides 
07.02.2007Espen H. Lian  3B  Fair Transition Systems, SPL semantics  Slides 
14.02.2007Espen H. Lian  3B  Linear Temporal Logic  Slides 
21.02.2007Espen H. Lian   3B  Proof methods, Logic  Proof methods Slides

Branching-time temporal logic and modal logic Slides 

28.02.2007Gerardo Schneider  3B  Model Checking - Foundations  Automata & Logic (Holzmann Chap. 6) Slides

Distribution of papers 

07.03.2007Gerardo Schneider  3B  Foundations, Promela  LTL into Automata (Peled Chap. 6)

Overview of Promela (Holzmann Chap. 2 & 3) Slides 

14.03.2007Gerardo Schneider  3B  Promela  Promela Semantics (Holzmann Chap. 7)Slides 
19.03.2007Gerardo Schneider  Forskningsparken - 16:00-19:00  Promela  Correctness claims (Holzmann Chap. 4) Slides 
22.03.2007Gerardo Schneider  To be defined  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) 

04.04.2007      Easter 
11.04.2007Espen  3B  Temporal Logic, Proof Systems  Exercises 
18.04.2007Espen & Gerardo  3B  Paper Presentation  Cristian: Mu-calculus model checking

Joakim: Abstract Interpretation  

25.04.2007Espen & Gerardo  3B  Mandatory Assignment   
02.05.2007Espen & Gerardo  3B  Paper presentation  Jarle: CTL model checking

Hallstein: Model checking timed automata 

09.05.2007Espen & Gerardo  3B  Mandatory Assignment   
16.05.2007Espen & Gerardo  3B  Mandatory Assignment  Mandatory Assignment: Delivery 
23.05.2007Gerardo Schneider  3B  Final Remarks  Great debates Slides 
30.05.2007Espen & Gerardo  3B  Exam   
Publisert 10. jan. 2007 14:12 - Sist endret 28. sep. 2007 17:16