Write a Blog >>
Wed 22 Jan 2020 14:00 - 14:21 at Ile de France II (IDF II) - Program Logics Chair(s): Azalea Raad

Early in the development of Hoare logic, Owicki and Gries introduced auxiliary variables as a way of encoding information about the history of a program’s execution that is useful for verifying its correctness. Over a decade later, Abadi and Lamport observed that it is sometimes also necessary to know in advance what a program will do in the future. To address this need, they proposed prophecy variables, originally as a proof technique for refinement mappings between state machines. However, despite the fact that prophecy variables are a clearly useful reasoning mechanism, there is (surprisingly) almost no work that attempts to integrate them into Hoare logic. In this paper, we present the first account of prophecy variables in a Hoare-style program logic that is flexible enough to verify logical atomicity (a relative of linearizability) for classic examples from the concurrency literature like RDCSS and the Herlihy-Wing queue. Our account is formalized in the Iris framework for separation logic in Coq. It makes essential use of ownership to encode the exclusive right to resolve a prophecy, which in turn enables us to enforce soundness of prophecies with a very simple set of proof rules.

Wed 22 Jan

Displayed time zone: Saskatchewan, Central America change

14:00 - 15:05
Program LogicsResearch Papers at Ile de France II (IDF II)
Chair(s): Azalea Raad MPI-SWS, Germany
14:00
21m
Talk
The Future is Ours: Prophecy Variables in Separation Logic
Research Papers
Ralf Jung MPI-SWS, Rodolphe Lepigre MPI-SWS, Gaurav Parthasarathy ETH Zurich, Marianna Rapoport University of Waterloo, Amin Timany imec-Distrinet KU-Leuven, Derek Dreyer MPI-SWS, Bart Jacobs imec-DistriNet, Dept. CS, KU Leuven
Link to publication DOI Media Attached
14:21
21m
Talk
Spy Game: Verifying a Local Generic Solver in Iris
Research Papers
Paulo Emílio de Vilhena Inria, François Pottier Inria, France, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud
Link to publication DOI Media Attached File Attached
14:43
21m
Talk
Actris: Session-Type Based Reasoning in Separation Logic
Research Papers
Jonas Kastberg Hinrichsen IT University of Copenhagen, Jesper Bengtson IT University of Copenhagen, Robbert Krebbers Delft University of Technology
Link to publication DOI Media Attached File Attached