Model-Checking SS 2012

News | Basic information | Content | Exercises | Slides | Links

Lecture 2 (23.04.2012)

• Slide2.1
• Slide2.2
• Slide2.3
• Slide2.4

Lecture 3 (24.04.2012)

• Slide3.1
• Slide3.2
• Slide3.3
• Slide3.4
• Slide3.5
• Inductive Safety and Termination Arguments

Lecture 4 (30.04.2012)

• Reachability Computation
• Slide4.3
• Slide4.4

Lecture 5 (07.05.2012)

• Abstraction for Reachability Computation
• Slide5.1
• Slide5.2
• Slide5.3
• Slide5.4

Lecture 6 (08.05.2012)

• Abstract Reachability Algorithm
• Slide6.1
• Slide6.2
• Slide6.3
• Slide6.4

Lecture 7 (14.05.2012)

• Abstraction Refinment using Spurious Counterexamples
• Slide7.1
• Slide7.2
• Slide7.3

Lectures 1 - 7 in one file

Lecture 8 (21.05.2012)

• Section 2 and 3
• Slide8.1
• Slide8.2
• Slide8.3
• Slide8.4

Lecture 9 (22.05.2012)

• Reachability and Summary for Programs with Procedures
• Slide9.1
• Slide9.2
• Slide9.3
• Slide9.4

Lecture 10 (04.06.2012)

• Slide10.1
• Slide10.2
• Slide10.3
• Slide10.4
• Slide10.5

Lecture 11 (05.06.2012)

• Slide11.1
• Slide11.2
• Slide11.3

Lecture 12 (11.06.2012)

• Slide12.1
• Slide12.2
• Slide12.3
• Slide12.4

Lecture 13 (12.06.2012)

• Slide13.1
• Slide13.2

Lecture 14 (18.06.2012)

• Slide14.1
• Slide14.2
• Slide14.3
• Slide14.4

Lecture 15 (19.06.2012)

• Functional programming language, syntax, base typing, evaluation
• Slide15.1
• Slide15.2
• Slide15.3
• Slide15.4
• Slide15.5

Lecture 16 (25.06.2012)

• Refinement types
• Slide16.1
• Slide16.2
• Slide16.3
• Slide16.4
• Slide16.5

Lecture 17 (26.06.2012)

• Slide17

Lecture 18 (02.07.2012)

• Slide18