Undervisningsplan

DatoUndervises avStedTemaKommentarer / ressurser
25.01.2006Gerardo Schneider    Introduction  Introduction to Formal Methods

Slides 

01.02.2006Espen H. Lian    Background  First Order Logic, SPL syntax, Hoare Logic

Andrews Chap. 2, Manna & Pnueli Chap. 0

Slides

Slides (multi4) 

08.02.2006Espen H. Lian    Temporal Logic  Fair Transition Systems, SPL semantics

Manna & Pnueli Chap. 0

Slides

Slides (multi4) 

15.02.2006Espen H. Lian    Temporal Logic  Temporal Logic

Manna & Pnueli Chap. 0

Slides

Slides(multi4)

Mandatory Assignment 1 

22.02.2006Espen H. Lian    Temporal Logic  Proof methods

Manna & Pnueli's paper

Slides

Slides (multi4) 

01.03.2006Espen H. Lian    Temporal Logic  CTL* and Modal Logic

Slides

Slides (multi4)

Kropf Chap. 4 

08.03.2006Gerardo Schneider    Model Checking - Foundations  Automata & Logic

Holzmann Chap. 6

Distribution of research papers

Slides 

15.03.2006    No lecture  Fagkritisk dag

Mandatory Assignment 1: Hand-in 

22.03.2006    No lecture   
29.03.2006Gerardo Schneider    Foundations / Promela  LTL into Automata (Peled Chap. 6)

Overview of Promela (Holzmann Chap. 2 & 3)

Mandatory Assignment 2: Delivery

Slides

Mandatory Assignment 2 Promela Model for Exercise 1 

05.04.2006Gerardo Schneider    Promela  Promela Semantics

Holzmann Chap. 7

Slides 

12.04.2006    No lecture  Easter (Påske) 
19.04.2006Espen H. Lian    Promela  Assignment 2 
26.04.2006Gerardo Schneider    Promela  Correctness claims

Holzmann Chap. 4

Slides 

03.05.2006Gerardo Schneider    Model Checking  Algorithms and Final Remarks

Part 0 (Administ.): Slides

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

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

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

Part 3 (Great Debates): Slides

 

10.05.2006Espen & Gerardo    Paper presentation  Timed Automata: Marius

Mu-calculus: Zeljko 

17.05.2006    No lecture  Grunnlovsdag 
24.05.2006Espen & Gerardo    Paper presentation  Abstract Interpretation: Ragnhild

Assumption-Commitment: Erik

CTL Model Checking: Eline 

31.05.2006Espen & Gerardo    Revision   
02.06.2006    Exam   
Publisert 6. des. 2005 12:49 - Sist endret 3. mai 2006 17:26