Thibault Dardinier

According to our database, Thibault Dardinier authored at least 33 papers between 2018 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2026

Hyper Separation Logic (extended version).

Trayan Gospodinov, Peter Müller, Thibault Dardinier

CoRR, April, 2026

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version).

Hongyi Ling, Thibault Dardinier, Ellen Arlt, Peter Müller

CoRR, March, 2026

2025

PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs.

Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy

Proc. ACM Program. Lang., 2025

Formal Foundations for Translational Separation Logic Verifiers.

Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller

Proc. ACM Program. Lang., 2025

2024

Formal Foundations for Translational Separation Logic Verifiers - Artifact.

Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller

Dataset, October, 2024

Hypra: A Deductive Program Verifier for Hyperproperties (artifact).

Thibault Dardinier, Anqi Li, Peter Müller

Dataset, July, 2024

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (artifact).

Thibault Dardinier, Peter Müller

Dataset, March, 2024

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (artifact).

Thibault Dardinier, Peter Müller

Dataset, March, 2024

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language.

Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers

Proc. ACM Program. Lang., 2024

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties.

Thibault Dardinier, Peter Müller

Proc. ACM Program. Lang., 2024

Hypra: A Deductive Program Verifier for Hyper Hoare Logic.

Thibault Dardinier, Anqi Li, Peter Müller

Proc. ACM Program. Lang., 2024

Formal Foundations for Translational Separation Logic Verifiers (extended version).

Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller

CoRR, 2024

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version).

Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers

CoRR, 2024

2023

Verification-Preserving Inlining in Automatic Separation Logic Verifiers.

Thibault Dardinier, Gaurav Parthasarathy, Peter Müller

Proc. ACM Program. Lang., April, 2023

CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity (Artifact).

Marco Eilers, Thibault Dardinier, Peter Müller

Dataset, March, 2023

CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity.

Marco Eilers, Thibault Dardinier, Peter Müller

Proc. ACM Program. Lang., 2023

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version).

Thibault Dardinier, Peter Müller

CoRR, 2023

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

Thibault Dardinier

Arch. Formal Proofs, 2023

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

Thibault Dardinier

Arch. Formal Proofs, 2023

2022

Sound Automation of Magic Wands (Artifact).

Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers

Dataset, May, 2022

Sound Automation of Magic Wands (Artifact).

Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers

Dataset, May, 2022

Fractional resources in unbounded separation logic.

Thibault Dardinier, Peter Müller, Alexander J. Summers

Proc. ACM Program. Lang., 2022

Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version).

Thibault Dardinier, Gaurav Parthasarathy, Peter Müller

CoRR, 2022

Sound Automation of Magic Wands (extended version).

Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Alexander J. Summers, Peter Müller

CoRR, 2022

Unbounded Separation Logic.

Thibault Dardinier

Arch. Formal Proofs, 2022

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

Thibault Dardinier

Arch. Formal Proofs, 2022

Formalization of a Framework for the Sound Automation of Magic Wands.

Thibault Dardinier

Arch. Formal Proofs, 2022

VeriMon: A Formally Verified Monitoring Tool.

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

Proceedings of the Theoretical Aspects of Computing - ICTAC 2022, 2022

Sound Automation of Magic Wands.

Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers

Proceedings of the Computer Aided Verification - 34th International Conference, 2022

2020

Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations.

Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider, Dmitriy Traytel

Arch. Formal Proofs, 2020

A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic.

David A. Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Formalization of Multiway-Join Algorithms.

Thibault Dardinier

Arch. Formal Proofs, 2019

2018

A new analysis method for evolutionary optimization of dynamic and noisy objective functions.

Raphaël Dang-Nhu, Thibault Dardinier, Benjamin Doerr, Gautier Izacard, Dorian Nogneng

Proceedings of the Genetic and Evolutionary Computation Conference, 2018