Follow
Thibault Dardinier
Thibault Dardinier
Verified email at inf.ethz.ch - Homepage
Title
Cited by
Cited by
Year
A formally verified, optimized monitor for metric first-order dynamic logic
D Basin, T Dardinier, L Heimes, S Krstić, M Raszyk, J Schneider, D Traytel
Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris …, 2020
362020
A new analysis method for evolutionary optimization of dynamic and noisy objective functions
R Dang-Nhu, T Dardinier, B Doerr, G Izacard, D Nogneng
Proceedings of the Genetic and Evolutionary Computation Conference, 1467-1474, 2018
312018
Sound automation of magic wands
T Dardinier, G Parthasarathy, N Weeks, P Müller, AJ Summers
International Conference on Computer Aided Verification, 130-151, 2022
142022
Hyper Hoare Logic:(dis-) proving program hyperproperties (extended version)
T Dardinier, P Müller
arXiv preprint arXiv:2301.10037, 2023
102023
Fractional resources in unbounded separation logic
T Dardinier, P Müller, AJ Summers
Proceedings of the ACM on Programming Languages 6 (OOPSLA2), 1066-1092, 2022
102022
VeriMon: a formally verified monitoring tool
D Basin, T Dardinier, N Hauser, L Heimes, JJ Huerta y Munive, ...
International Colloquium on Theoretical Aspects of Computing, 1-6, 2022
62022
Verification-preserving inlining in automatic separation logic verifiers
T Dardinier, G Parthasarathy, P Müller
Proceedings of the ACM on Programming Languages 7 (OOPSLA1), 789-818, 2023
32023
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
M Eilers, T Dardinier, P Müller
Proceedings of the ACM on Programming Languages 7 (PLDI), 1682-1707, 2023
22023
Formalization of Hyper Hoare Logic: A Logic to (Dis-) Prove Program Hyperproperties
T Dardinier
Arch. Formal Proofs 2023, 2023
12023
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
T Dardinier, L Heimes, M Raszyk, J Schneider, D Traytel
Arch. Formal Proofs (Apr. 2020). Formal proof development. url: https://isa …, 2023
12023
Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs
T Dardinier
Archive of Formal Proofs, March, issn, 2023
12023
Unbounded Separation Logic
T Dardinier
Archive of Formal Proofs, September, issn, 2022
12022
Beyond the frame rule: Static inlining in separation logic
T Dardinier
ETH Zurich, 2020
12020
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
G Parthasarathy, T Dardinier, B Bonneau, P Müller, AJ Summers
arXiv preprint arXiv:2404.03614, 2024
2024
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand
T Dardinier
2023
Formalization of a Framework for the Sound Automation of Magic Wands
T Dardinier
2023
Formalization of Multiway-Join Algorithms
T Dardinier
2023
The system can't perform the operation now. Try again later.
Articles 1–17