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

We verify the partial correctness of a “local generic solver”, that is, an on-demand, incremental, memoizing least fixed point computation algorithm. The verification is carried out in Iris, a modern breed of concurrent separation logic. The specification is simple: the solver computes the optimal least fixed point of a system of monotone equations. Although the solver relies on mutable internal state for memoization and for “spying”, a form of dynamic dependency discovery, it is apparently pure: no side effects are mentioned in its specification. As auxiliary contributions, we provide several illustrations of the use of prophecy variables, a novel feature of Iris; we establish a restricted form of the infinitary conjunction rule; and we provide a specification and proof of Longley’s modulus function, an archetypical example of spying.

Presentation Slides (talk.pdf)336KiB

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
21m
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
21m
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
21m
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