Verification Seminar, Summer Semester 2009/2010
Lecturer:
Prof. C. Kirsch and
Dr. A. Sokolova
Schedule: Thursdays 10am-12pm in T06
First meeting: Wednesday, March 10 at 3:30pm in T03
Language: English
The seminar may also be taken by PhD students
Seminar description: Verification of finite state concurrent systems such as sequential circuit designs and communication protocols has been a vivid research topic in computer science for the past 30 years. The main objective is obtaining a formal proof of correctness of a system. Via verification techniques, practically oriented computer scientists learn the need of abstraction and formal reasoning. Students interested in theory will get an introduction to formal methods research for specification and verification. In this seminar, students will be assigned research papers or broader verification topics, which they need to study, understand, and present in class.
Literature: t.b.a.
Prerequisites:
Knowledge of basics of theoretical computer science like logic for computer science or automata theory is an asset.
Exam: Continuous assessment.
Schedule:
- 10th of March 2010, first meeting
- 18th of March 2010, choice of papers, global discussion
- 22nd of April 2010, Ana Sokolova presenting the paper "Bisimulation through probabilistic testing" by Larsen and Skou
- 29th of April 2010, Martin Aigner presenting the paper "A lock-free, concurrent, and incremental stack
scanning mechanism for garbage collectors" by Kliot, Petrank, and Steensgaard
- 20th of May, Andreas Haas presenting the paper "Bounded model checking" by Biere et al.
- 27th of May, Andreas Schoenegger presenting the paper "A notion of glue expressiveness for
component-based systems" by Bliudze and Sifakis.