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 (GECCO, 2018)

Formalization of Multiway-Join Algorithms. - Thibault Dardinier (Arch. Formal Proofs, 2019)

A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic. - David A. Basin; Thibault Dardinier; Lukas Heimes; Srdan Krstic; Martin Raszyk; Joshua Schneider 001; Dmitriy Traytel (IJCAR (1), 2020)

Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations. - Thibault Dardinier; Lukas Heimes; Martin Raszyk; Joshua Schneider 001; Dmitriy Traytel (Arch. Formal Proofs, 2020)

Sound Automation of Magic Wands. - Thibault Dardinier; Gaurav Parthasarathy; Noé Weeks; Peter Müller 001; Alexander J. Summers (CAV (2), 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 001; Dawit Legesse Tirore; Dmitriy Traytel; et al. (ICTAC, 2022)

Formalization of a Framework for the Sound Automation of Magic Wands. - 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)

Unbounded Separation Logic. - Thibault Dardinier (Arch. Formal Proofs, 2022)

Sound Automation of Magic Wands (extended version). - Thibault Dardinier; Gaurav Parthasarathy; Noé Weeks; Alexander J. Summers; Peter Müller 001 (CoRR, 2022)

Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version). - Thibault Dardinier; Gaurav Parthasarathy; Peter Müller 001 (CoRR, 2022)

Fractional resources in unbounded separation logic. - Thibault Dardinier; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2022)

Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs. - Thibault Dardinier (Arch. Formal Proofs, 2023)

Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties. - Thibault Dardinier (Arch. Formal Proofs, 2023)

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). - Thibault Dardinier; Peter Müller 001 (CoRR, 2023)

CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity. - Marco Eilers; Thibault Dardinier; Peter Müller 001 (Proc. ACM Program. Lang., 2023)

Verification-Preserving Inlining in Automatic Separation Logic Verifiers. - Thibault Dardinier; Gaurav Parthasarathy; Peter Müller 001 (Proc. ACM Program. Lang., 2023)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version). - Gaurav Parthasarathy; Thibault Dardinier; Benjamin Bonneau; Peter Müller 001; Alexander J. Summers (CoRR, 2024)

Formal Foundations for Translational Separation Logic Verifiers (extended version). - Thibault Dardinier; Michael Sammler; Gaurav Parthasarathy; Alexander J. Summers; Peter Müller 001 (CoRR, 2024)

Hypra: A Deductive Program Verifier for Hyper Hoare Logic. - Thibault Dardinier; Anqi Li; Peter Müller 001 (Proc. ACM Program. Lang., 2024)

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. - Thibault Dardinier; Peter Müller 001 (Proc. ACM Program. Lang., 2024)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. - Gaurav Parthasarathy; Thibault Dardinier; Benjamin Bonneau; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2024)

Formal Foundations for Translational Separation Logic Verifiers. - Thibault Dardinier; Michael Sammler; Gaurav Parthasarathy; Alexander J. Summers; Peter Müller 001 (Proc. ACM Program. Lang., 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)