Fri 12 Jan 2018 16:15 - 16:40 at Watercourt - Types for State Chair(s): Neel Krishnaswami

We provide a practical way to ease the verification of programs whose state evolves monotonically. The main idea is that a property witnessed in a prior state can be recalled in the current state, provided (1) state evolves according to a given preorder, and (2) the property is preserved by this preorder. In many realistic scenarios, such monotonic reasoning yields concise modular proofs, saving the need for explicit program invariants. We distill our approach into the monotonic-state monad, a general yet compact interface for Hoare-style reasoning about monotonic state in a dependently typed language. We prove the soundness of the monotonic-state monad and use it as a unified foundation for reasoning about monotonic state in the F* verification system. Based on this foundation, we build libraries for various mutable data structures like monotonic references and apply these libraries at scale to the verification of several distributed applications.

Fri 12 Jan
Times are displayed in time zone: Tijuana, Baja California change

15:50 - 17:05: Types for StateResearch Papers at Watercourt
Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge
15:50 - 16:15
A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Research Papers
Amin Timanyimec-Distrinet KU-Leuven, Leo StefanescoENS Lyon, Morten Krogh-JespersenAarhus University, Lars BirkedalAarhus University
16:15 - 16:40
Recalling a Witness: Foundations and Applications of Monotonic State
Research Papers
Danel AhmanInria Paris, Cédric FournetMicrosoft Research, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris and ENS Paris, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
16:40 - 17:05
RustBelt: Securing the Foundations of the Rust Programming Language
Research Papers
Ralf JungMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Robbert KrebbersDelft University of Technology, Derek DreyerMPI-SWS