Keynote talk I

I- A Hierarchy of Thread-Modular Proof Systems

podelsky Andreas Podelski
University of Freiburg, Germany

Biography:
Andreas Podelski works in the area of programming languages, specifically on program analysis and verification.  He is an Associate Editor of the journals ToPLaS, FMSD, JAR, and STTT.  He has served as the chair or as a member of the program committee of over 50 conferences and he has been the invited plenary speaker at over 20 conferences.   He did his education at Münster, Germany (MS), Paris, France (PhD), and Berkeley, CA  (PostDoc).  He has spent sabbaticals for research at MSR Redmond, ENS Paris, MSR Cambridge, and Stanford Research Institute.

Abstract:
Verifying concurrent programs against safety properties is a fundamental problem. Bugs in concurrent programs can arise due to unanticipated schedules between threads. In practice, such bugs are difficult to test for, reproduce, or debug. A naive approach to verification constructs a sequential program that runs all possible interleavings of the threads in the original program (the “product construction”).  The product construction approach does not scale because the number of potential schedules grows exponentially with the number of threads. More seriously, the product construction does not work in the parameterized setting, in which we want to verify a program no matter how many threads are running in parallel.

The classical approach to verification of concurrent programs uses a different, modular, approach. In this approach, one reasons about a single thread of the original program, summarizing the effect of all other threads that run in parallel.  This approach, called thread-modular reasoning in the world of model checking and the Owicki–Gries proof system in the world of program logics, can prove safety properties of many parameterized multi-threaded programs. Indeed, thread-modular reasoning is the basis for many software verification tools.

However, it is well-known that thread-modular reasoning is incomplete: a program may satisfy a safety property but there may not be a thread-modular proof demonstrating it. The incompleteness is not a theoretical curiosity —many practical examples do not have thread-modular proofs.   In this talk, we will describe a hierarchy of proof systems that are suitable for those practical examples while retaining the nice modularity properties of thread-modular reasoning.

This is joint work with Jürgen Christ, Jochen Hoenicke, and Rupak Majumdar.

Dates

These are firm deadlines

January 12, 2016

Abstract submission deadline

January 23, 2016

Paper submission deadline

March 15, 2016

Acceptance notification

April 05, 2016

Camera ready copy due

Proceedings

SpringerLNCS

The proceedings of the conference will be published in Springer’s Lecture Notes in Computer Science

Partners & Sponsors

SponsorsNETYS28