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: (GMT-06:00) Saskatchewan, Central America change

14:00 - 15:05: Research Papers - Program Logics at Ile de France II (IDF II)
Chair(s): Azalea RaadMPI-SWS, Germany
POPL-2020-Research-Papers14:00 - 14:21
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
POPL-2020-Research-Papers14:21 - 14:43
Paulo Emílio de VilhenaInria, François PottierInria, France, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers14:43 - 15:05
Jonas Kastberg HinrichsenIT University of Copenhagen, Jesper BengtsonIT University of Copenhagen, Robbert KrebbersDelft University of Technology
Link to publication DOI Media Attached File Attached