5109
Comment:
|
5302
|
Deletions are marked like this. | Additions are marked like this. |
Line 3: | Line 3: |
'''Instructors:''' Viktor Vafeiadis and Derek Dreyer | '''Instructors:''' [[http://www.mpi-sws.org/~viktor|Viktor Vafeiadis]] and [[http://www.mpi-sws.org/~dreyer|Derek Dreyer]] |
Line 5: | Line 5: |
'''Meeting Time:''' 2 hours, once a week | '''Teaching assistant:'' [[http://www.mpi-sws.org/~neis|Georg Neis]] '''Meeting time:''' 2 hours, once a week, April - July 2011 |
Line 20: | Line 22: |
|| Monday 2011-05-02, 16:15. || Owicki-Gries (Jonas) || [example] || | || Monday 2011-05-02, 16:15. || Owicki-Gries (Jonas) || [[attachment:owicki-example.pdf|example]] || |
Line 43: | Line 45: |
* Viktor Vafeiadis: Modular fine-grained concurrency verification. PhD thesis. [[attachment:vthesis-rg.pdf|Sections 2.2 and 2.3 only.]] [[http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-726.pdf|[entire thesis]]] | * Viktor Vafeiadis: Modular fine-grained concurrency verification. PhD thesis. [[attachment:vthesis-rg.pdf|Sections 2.2 and 2.3 only.]] ([[http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-726.pdf|entire thesis]]) |
Concurrent Program Logics
Instructors: Viktor Vafeiadis and Derek Dreyer
Teaching assistant: Georg Neis Meeting time: 2 hours, once a week, April - July 2011
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.
Monday 2011-04-11, 12:15. Introduction, Hoare logic (Viktor) 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) Monday 2011-05-09, 16:15. Rely-guarantee (Georg) Monday 2011-05-16, 16:15. Separation logic (Sigurd) Monday 2011-05-23, 12:15. Concurrent separation logic Monday 2011-05-30, 16:15. Permissions Monday 2011-06-06, 16:15. Abstract predicates Monday 2011-06-13, 16:15. Storable locks Monday 2011-06-20. No meeting (LICS) Monday 2011-06-27, 16:15. RGSep Monday 2011-07-04, 16:15. More RGSep, LRG Monday 2011-07-11, 16:15. Deny-guarantee Monday 2011-07-18, 16:15. Concurrent abstract predicates Monday 2011-07-25, 16:15. More DG
Susan Owicki, David Gries: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319-340 (1976)
Viktor Vafeiadis: Modular fine-grained concurrency verification. PhD thesis. Sections 2.2 and 2.3 only. (entire thesis) Joey W. Coleman, Cliff B. Jones: A structural proof of the soundness of rely/guarantee rules. Journal of Logic and Computation 17: 807-841 (2007) Leonor Prensa Nieto: The rely-guarantee method in Isabelle/HOL. ESOP 2003.
Abstract
Schedule
Reading list
Early papers
Rely/guarantee
Separation logic
Hypothetical frame rule, abstract predicates
Concurrent Separation Logic
Permissions
Storable locks
RGSep, LRG
Deny-guarantee, concurrent abstract predicates