Zusammenfasssung:
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.
Kurzbiographie von Prof. Dr. Peter Müller
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. (<link www.pm.inf.ethz.ch/people/pmueller&gt;http://www.pm.inf.ethz.ch/people/pmueller </link>)