Thibault Dardinier

Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties

by Thibault Dardinier

Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs

by Thibault Dardinier

Unbounded Separation Logic

by Thibault Dardinier

A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand

by Thibault Dardinier

Formalization of a Framework for the Sound Automation of Magic Wands

by Thibault Dardinier

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

Formalization of Multiway-Join Algorithms

by Thibault Dardinier