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
392020
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
352018
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
182022
Hyper Hoare Logic:(Dis-) Proving Program Hyperproperties
T Dardinier, P Müller
Proceedings of the ACM on Programming Languages 8 (PLDI), 1485-1509, 2024
152024
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
122022
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
82022
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
42023
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
42023
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
G Parthasarathy, T Dardinier, B Bonneau, P Müller, AJ Summers
Proceedings of the ACM on Programming Languages 8 (PLDI), 1510-1534, 2024
22024
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
22023
Formalization of Hyper Hoare Logic: A Logic to (Dis-) Prove Program Hyperproperties
T Dardinier
Arch. Formal Proofs 2023, 2023
22023
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 …, 2024
12024
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
Formal Foundations for Translational Separation Logic Verifiers (extended version)
T Dardinier, M Sammler, G Parthasarathy, AJ Summers, P Müller
arXiv preprint arXiv:2407.20002, 2024
2024
A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand
T Dardinier
2024
Formalization of a Framework for the Sound Automation of Magic Wands
T Dardinier
2024
Formalization of Multiway-Join Algorithms
T Dardinier
2024
Hypra: A Deductive Program Verifier for Hyper Hoare Logic
T DARDINIER, A LI, P MÜLLER
2024
The system can't perform the operation now. Try again later.
Articles 1–19