Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties by Thibault Dardinier Apr 03
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs by Thibault Dardinier Mar 15
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand by Thibault Dardinier May 30
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations by Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider and Dmitriy Traytel Apr 09