Campus Event Calendar

Event Entry

What and Who

Modular Verification of Finite Blocking

Peter Müller
ETH Zürich
SWS Colloquium

Peter Müller has been Full Professor and head of the Chair of Programming Methodology at ETH Zurich since August 2008. His research focuses on languages, techniques, and tools for the development of correct software. His previous appointments include a position as Researcher at Microsoft Research in Redmond, an Assistant Professorship at ETH Zurich, and a position as Project Manager at Deutsche Bank in Frankfurt. Peter Müller received his PhD from the University of Hagen.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
AG Audience

Date, Time and Location

Thursday, 29 August 2013
60 Minutes


Finite blocking is an important correctness property of multi-threaded programs. It requires that each blocking operation such as acquiring a lock or joining a thread executes eventually. In addition to deadlock freedom, finite blocking in the presence of non-terminating threads requires one to prove that no thread holds a lock indefinitely or attempts to join a non-terminating thread. In this talk, I will present a verification technique for finite blocking of possibly non-terminating programs. The key idea is to track explicitly whether a thread has an obligation to perform an operation that releases another thread from being blocked, for instance, an obligation to release a lock or to terminate. Each obligation is associated with a lifetime to ensure that it is fulfilled within finitely many steps. Our technique guarantees finite blocking for programs with a finite number of threads and fair scheduling. We have implemented our technique in the automatic program verifier Chalice.


Rupak Majumdar
--email hidden

Video Broadcast

E1 5
passcode not visible
logged in users only

Susanne Girard, 08/28/2013 09:37
Susanne Girard, 08/27/2013 15:51 -- Created document.