Thibault Dardinier

26 papers A 1C 1Journal 22Unranked 2
YearRankTypeTitle / Venue / Authors
2026 J jnl
Sound State Encodings in Translational Separation Logic Verifiers (Extended Version).
CoRR
Hongyi Ling, Thibault Dardinier, Ellen Arlt, Peter Müller
2025 J jnl
Formal Foundations for Translational Separation Logic Verifiers.
Proc. ACM Program. Lang.
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
2025 J jnl
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs.
Proc. ACM Program. Lang.
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
2024 J jnl
Formal Foundations for Translational Separation Logic Verifiers (extended version).
CoRR
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
2024 J jnl
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties.
Proc. ACM Program. Lang.
Thibault Dardinier, Peter Müller
2024 J jnl
Hypra: A Deductive Program Verifier for Hyper Hoare Logic.
Proc. ACM Program. Lang.
Thibault Dardinier, Anqi Li, Peter Müller
2024 J jnl
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version).
CoRR
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers
2024 J jnl
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language.
Proc. ACM Program. Lang.
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers
2023 J jnl
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity.
Proc. ACM Program. Lang.
Marco Eilers, Thibault Dardinier, Peter Müller
2023 J jnl
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs.
Arch. Formal Proofs
Thibault Dardinier
2023 J jnl
Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties.
Arch. Formal Proofs
Thibault Dardinier
2023 J jnl
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version).
CoRR
Thibault Dardinier, Peter Müller
2023 J jnl
Verification-Preserving Inlining in Automatic Separation Logic Verifiers.
Proc. ACM Program. Lang.
Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
2022 J jnl
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand.
Arch. Formal Proofs
Thibault Dardinier
2022 J jnl
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity.
CoRR
Marco Eilers, Thibault Dardinier, Peter Müller
2022 J jnl
Formalization of a Framework for the Sound Automation of Magic Wands.
Arch. Formal Proofs
Thibault Dardinier
2022 J jnl
Fractional resources in unbounded separation logic.
Proc. ACM Program. Lang.
Thibault Dardinier, Peter Müller, Alexander J. Summers
2022 J jnl
Sound Automation of Magic Wands (extended version).
CoRR
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Alexander J. Summers, Peter Müller
2022 — conf
Sound Automation of Magic Wands.
CAV (2)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers
2022 J jnl
Unbounded Separation Logic.
Arch. Formal Proofs
Thibault Dardinier
2022 C conf
VeriMon: A Formally Verified Monitoring Tool.
ICTAC
David A. Basin, Thibault Dardinier, Nico Hauser, Lukas Heimes, Jonathan Julián Huerta y Munive, Nicolas Kaletsch, Srdan Krstic, Emanuele Marsicano, Martin Raszyk, Joshua Schneider, Dawit Legesse Tirore, Dmitriy Traytel, Sheila Zingg
2022 J jnl
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version).
CoRR
Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
2020 — conf
A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic.
IJCAR (1)
David A. Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
2020 J jnl
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations.
Arch. Formal Proofs
Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
2019 J jnl
Formalization of Multiway-Join Algorithms.
Arch. Formal Proofs
Thibault Dardinier
2018 A conf
A new analysis method for evolutionary optimization of dynamic and noisy objective functions.
GECCO
Raphaël Dang-Nhu, Thibault Dardinier, Benjamin Doerr, Gautier Izacard, Dorian Nogneng