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

Message passing is a useful abstraction to implement concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs that use a combination of the aforementioned features. Actris combines the power of modern concurrent separation logics with a first-class protocol mechanism—based on session types—for reasoning about message passing in the presence of other concurrency paradigms. We show that Actris provides a suitable level of abstraction by proving functional correctness of a variety of examples, including a distributed merge sort, a distributed load-balancing mapper, and a variant of the map-reduce model, using relatively simple specifications. Soundness of Actris is proved using a model of its protocol mechanism in the Iris framework. We mechanised the theory of Actris, together with tactics for symbolic execution of programs, as well as all examples in the paper, in the Coq proof assistant.

slides (main.pdf)695KiB

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