Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties
by Thibault Dardinier 📧
by Thibault Dardinier 📧
Thibault Dardinier
Homepages 🌐
E-Mails 📧
Entries
2023
by Thibault Dardinier 📧
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs
by Thibault Dardinier 📧
2022
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand
by Thibault Dardinier 🌐
2020
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 🌐