Informatik, TU Wien

Automatic Verification of Concurrent Programs in Chalice

Advanced multi-threaded programs apply concurrency concepts in sophisticated ways.

Der Arbeitsbereich für Programmiersprachen und Übersetzer am Institut für Computersprachen lädt zu folgendem Vortrag ein:


Advanced multi-threaded programs apply concurrency concepts in sophisticated ways. For instance, they use fine-grained locking to increase parallelism and change locking orders dynamically when data structures are being reorganized. This talk presents a sound and modular verification methodology that can handle advanced concurrency patterns in multi-threaded, object-based programs. The methodology is based on implicit dynamic frames and uses fractional permissions to support fine-grained locking. It supports concepts such as multi-object monitor invariants, thread-local and shared objects, thread pre- and postconditions, and deadlock prevention with a dynamically changeable locking order. Our methodology is implemented in the Chalice program verifier, which prescribes the generation of verification conditions in first-order logic, well-suited for scrutiny
by off-the-shelf SMT solvers.


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.


Tee: 14:30 Uhr in der Bibliothek E185.1, Argentinierstr. 8, 4. Stock (Mitte).