Thibault Dardinier

Publication Activity (10 Years)

Years Active: 2018-2024
Publications (10 Years): 22

Top Topics

Information Flows

Concurrent Programs

Top Venues

Arch. Formal Proofs

Proc. ACM Program. Lang.

Publications

Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version). CoRR (2024)
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
Formal Foundations for Translational Separation Logic Verifiers (extended version). CoRR (2024)
Thibault Dardinier, Peter Müller
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Thibault Dardinier
Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties. Arch. Formal Proofs 2023 (2023)
Thibault Dardinier, Peter Müller
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). CoRR (2023)
Marco Eilers, Thibault Dardinier, Peter Müller
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Thibault Dardinier
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs. Arch. Formal Proofs 2023 (2023)
Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
Verification-Preserving Inlining in Automatic Separation Logic Verifiers. Proc. ACM Program. Lang. 7 (OOPSLA1) (2023)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers
Sound Automation of Magic Wands. CAV (2) (2022)
Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version). CoRR (2022)
Thibault Dardinier, Peter Müller, Alexander J. Summers
Fractional resources in unbounded separation logic. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Thibault Dardinier
Unbounded Separation Logic. Arch. Formal Proofs 2022 (2022)
Marco Eilers, Thibault Dardinier, Peter Müller
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity. CoRR (2022)
Thibault Dardinier
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand. Arch. Formal Proofs 2022 (2022)
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
VeriMon: A Formally Verified Monitoring Tool. ICTAC (2022)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Alexander J. Summers, Peter Müller
Sound Automation of Magic Wands (extended version). CoRR (2022)
Thibault Dardinier
Formalization of a Framework for the Sound Automation of Magic Wands. Arch. Formal Proofs 2022 (2022)
David A. Basin, Thibault Dardinier, Lukas Heimes, Srdan Krstic, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic. IJCAR (1) (2020)
Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations. Arch. Formal Proofs 2020 (2020)
Thibault Dardinier
Formalization of Multiway-Join Algorithms. Arch. Formal Proofs 2019 (2019)
Raphaël Dang-Nhu, Thibault Dardinier, Benjamin Doerr, Gautier Izacard, Dorian Nogneng
A new analysis method for evolutionary optimization of dynamic and noisy objective functions. GECCO (2018)