Die Dozenten der Informatik-Institute der Technischen Universität Braunschweig laden im Rahmen des Informatik-Kolloquiums zu folgendem Vortrag ein:
Prof. Dr. Heike Wehrheim, Universität Paderborn: Verification of concurrent lock-free algorithms
Beginn: 08.06.2011, 17:00 Uhr Ort: TU Braunschweig, Informatikzentrum, Mühlenpfordtstraße 23, 1.OG, Hörsaal M 160 Webseite: http://www.ibr.cs.tu-bs.de/cal/kolloq/2011-06-08-wehrheim.html Kontakt: Prof. Dr. Ursula Goltz
Concurrent algorithms are intrinsically difficult to get correct. Formal verification techniques present a way of establishing trust in the correctness by means of a mathematical proof. Currently, two approaches are being investigated in this area: model checking, a fully automatic proof of correctness which is however limited in the application domain, and interactive proving, which is not fully automatic but can treat a larger class of applications.
In the talk recent results on the verification of lock-free algorithms using the second approach are presented. Lock-free algorithms implement a concurrent access to standard data structures like stacks, queues or sets without locking the data structure. This lock-freedom allows for a high degree of concurrency, however, at the price of an increased complexity in verification.