Mon 8 Jan 2018 17:00 - 17:30 at Museum A - Proof Methods and Libraries Chair(s): René Thiemann

Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and game-based cryptographic security. By relying on SMT-based automation, unary weakest preconditions, user-defined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer.

Mon 8 Jan

CPP-2018
16:00 - 18:00: CPP 2018 - Proof Methods and Libraries at Museum A
Chair(s): René ThiemannUniversity of Innsbruck
CPP-201816:00 - 16:30
Talk
Craig McLaughlinThe University of Edinburgh, James McKinna, Ian StarkThe University of Edinburgh
DOI
CPP-201816:30 - 17:00
Talk
Talia RingerUniversity of Washington, Nathaniel YazdaniUniversity of Washington, Seattle, John LeoHalfaya Research, Dan GrossmanUniversity of Washington
DOI
CPP-201817:00 - 17:30
Talk
Niklas GrimmVienna University of Technology, Austria, Kenji MaillardInria Paris and ENS Paris, Cédric FournetMicrosoft Research, Cătălin HriţcuInria Paris, Matteo MaffeiSaarland University, Jonathan ProtzenkoMicrosoft Research, n.n., Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research, Santiago Zanella-BéguelinMicrosoft Research, n.n.
DOI
CPP-201817:30 - 18:00
Talk
Hugo FéréeUniversity of Kent, UK, Samuel HymUniversity of Lille, France, Micaela Mayero, Jean-Yves MoyenUniversity of Copenhagen, Denmark, David NowakCNRS, France
DOI