INF5140 - V?r 2011

Undervisningsplan

DatoUndervises avStedTemaKommentarer / ressurser
27.01.2011Gerardo Schneider? room 8270 PMA lab? Introduction? Slides - Plan

Slides - Introduction ?

03.02.2011Cristian Prisacariu? room 8270 PMA lab? First order logic and Modal logic? Slides ?
10.02.2011Cristian Prisacariu? room 8270 PMA lab? Dynamic logic? Slides?
17.02.2011Cristian Prisacariu? room 8270 PMA lab? Hoare Logic and Temporal logics? Slides?
24.02.2011Cristian Prisacariu? room 8270 PMA lab? Model Checking - Foundations? Automata & Logic (Holzmann Chap. 6)

Slides?

03.03.2011Cristian Prisacariu? room 8270 PMA lab? Model Checking - Foundations? Automata & Logic (Holzmann Chap. 6)

(continuation)?

10.03.2011Cristian Prisacariu? room 8270 PMA lab? Foundations, Promela? LTL into Automata (Peled Chap. 6)

Overview of Promela (Holzmann Chap. 2 & 3)

Slides?

22.03.2011Cristian Prisacariu? room 8270 PMA lab? Promela? Promela Semantics (Holzmann Chap. 7)

Slides?

24.03.2011Cristian Prisacariu? room 8270 PMA lab? Promela? Correctness claims (Holzmann Chap. 4)

Slides?

31.03.2011Cristian Prisacariu? room 8270 PMA lab? 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) ?

07.04.2011Cristian Prisacariu? NO teaching? Work on Project? Open door for discussion related to your mandatory assignment.?
14.04.2011Cristian Prisacariu? NO teaching? Work on Project? Open door for discussion related to your mandatory assignment.?
21.04.2011? ? EASTER? ?
28.04.2011Cristian Prisacariu? room 8270 PMA lab? Mandatory Assignment + Presentation Drafts? All students must show the drafts of their respective presentations.?
12.05.2011Gerardo Schneider? room 8270 PMA lab? Last lecture + Paper Presentation (day 1)? Last lecture: "Great debates" slides

Paper presentation:

Crystal Din: CTL model checking?

13.05.2011C. & G.? room 8270 PMA lab? Paper Presentation (day 2)? Paper presentations:

Martin Fagereng Johansen: Bounded Model Checking

Violet Pun: Mu-calculus model checking?

26.05.2011C. & G.? room 8270 PMA lab? 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.06.2011? ? Oral Examination ? ?
Publisert 27. jan. 2011 19:26 - Sist endret 23. mai 2011 13:55
Del p? e-post