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
Times are displayed in time zone: Saskatchewan, Central America change

14:00 - 15:05: Program LogicsResearch Papers at Ile de France II (IDF II)
Chair(s): Azalea RaadMPI-SWS, Germany
14:00 - 14:21
Talk
The Future is Ours: Prophecy Variables in Separation Logic
Research Papers
Ralf JungMPI-SWS, Rodolphe LepigreMPI-SWS, Gaurav ParthasarathyETH Zurich, Marianna RapoportUniversity of Waterloo, Amin Timanyimec-Distrinet KU-Leuven, Derek DreyerMPI-SWS, Bart Jacobsimec-DistriNet, Dept. CS, KU Leuven
Link to publication DOI Media Attached
14:21 - 14:43
Talk
Spy Game: Verifying a Local Generic Solver in Iris
Research Papers
Paulo Emílio de VilhenaInria, François PottierInria, France, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud
Link to publication DOI Media Attached File Attached
14:43 - 15:05
Talk
Actris: Session-Type Based Reasoning in Separation Logic
Research Papers
Jonas Kastberg HinrichsenIT University of Copenhagen, Jesper BengtsonIT University of Copenhagen, Robbert KrebbersDelft University of Technology
Link to publication DOI Media Attached File Attached