Model-Checking SS 2016

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

Lectures are accompanied by a weekly exercise lesson.

Exercise Sheets

• 14 Apr. 2016 : Exercise sheet #1 [PDF] Some useful links: Spin README Spin references Modex
• 21 Apr. 2016 : Exercise sheet #2 [PDF] [Solution] On LTL
• 28 Apr. 2016 : Exercise sheet #3 [PDF] [Solution 3.1 (1-3), Solution 3.1 (4-5), Solution 3.2] On Promela and Spin
• 12 May 2016 : Exercise sheet #4 [PDF] [Solution] More on LTL and Büchi automata
• 19 May 2016 : Exercise sheet #5 [PDF] [Solution] LTL to Büchi automata translation
• 31 May 2016 : No new sheets Continued with sheet #5
• 2 Jun. 2016 : Exercise sheet #6 [PDF] [Solution] Emptiness check
• 9 Jun. 2016 : Exercise sheet #7 [PDF] [Solution] Partial-order reduction
• 16 Jun. 2016 : Exercise sheet #8 [PDF] [Solution] CTL
• 23 Jun. 2016: Exercise sheet #9 [PDF] [Solution] NuSMV
• 28 Jun. 2016: Exercise sheet #10 [PDF] [Solution] BDDs
• 30 Jun. 2016: Exercise sheet #11 [PDF] [Solution] Abstraction, simulation and bisimulation
• Last week: Exercise sheet #12--13 [PDF] Abstraction refinement, pushdown systems