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