Concurrent Program Logics

Instructors: Viktor Vafeiadis and Derek Dreyer

Teaching assistant: Georg Neis

Meeting time: 2 hours, once a week, April - July 2011

Abstract

Reasoning about concurrent programming is a particularly exciting topic in program verification. The focus of much of the research in this area is on developing modular and compositional methods for verification that nonetheless allow for fine-grained synchronization, as well as the sharing of mutable data structures, between multiple threads. Although some of the fundamental ideas in the area (such as Hoare logic and rely-guarantee reasoning) were developed thirty years ago, there has been major progress in the last several years, and the field is complex and highly active.

In this seminar course, we will study the development of concurrent program logics, from their roots in the late '70s up to the most recent breakthrough technologies. The course will be structured like a reading group, with one student tasked with presenting a paper each week, followed by an in-depth discussion.

The course is being co-taught by Viktor Vafeiadis (MPI-SWS, the Kaiserslautern branch) and Derek Dreyer (MPI-SWS, the Saarbruecken branch), and will be conducted by videoconferencing between the two MPI-SWS locations.

Schedule

Date and time

Topic

Presenter

Files

Monday 2011-04-11, 12:15.

Introduction, Hoare logic

Viktor

slides

Monday 2011-04-17.

No meeting (Easter holiday)

Monday 2011-04-25.

No meeting (Easter holiday)

Monday 2011-05-02, 16:15.

Owicki-Gries

Jonas

slides example

Monday 2011-05-09, 16:15.

Rely-guarantee

Georg

slides example

Monday 2011-05-16, 16:15.

Separation logic

Sigurd

slides

Monday 2011-05-23, 12:15.

Concurrent separation logic

Beta

slides counter-example

Monday 2011-05-30, 16:15.

Permissions

Matt

slides(M) slides(V)

Monday 2011-06-06, 16:15.

Abstract predicates

Scott

slides

Thursday 2011-06-16, 16:15.

Storable locks

Derek

Monday 2011-06-20.

No meeting (LICS)

Thursday 2011-06-30, 16:15.

RGSep, LRG

Arthur

slides

Monday 2011-07-04, 16:15.

More RGSep, SmallfootRG

Viktor + Arthur

slides(V) slides(A)

Monday 2011-07-11.

No meeting (POPL deadline)

Monday 2011-07-18, 16:15.

Deny-guarantee

Georg

slides

Thursday 2011-07-21, 16:15.

Concurrent abstract predicates

Gil

slides

Thursday 2011-08-04, 16:15.

Concurrent abstract predicates (continued)

Gil

Reading list

Early papers

Rely/guarantee

Separation logic

Concurrent Separation Logic

Permissions

Hypothetical frame rule, abstract predicates

Storable locks

RGSep, LRG

Deny-guarantee

Concurrent abstract predicates

cpl (last edited 2011-07-25 23:44:25 by dreyer)