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 | 39 | 2020 |

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 | 35 | 2018 |

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 | 18 | 2022 |

Hyper Hoare Logic:(Dis-) Proving Program Hyperproperties T Dardinier, P Müller Proceedings of the ACM on Programming Languages 8 (PLDI), 1485-1509, 2024 | 15 | 2024 |

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 | 12 | 2022 |

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 | 8 | 2022 |

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 | 4 | 2023 |

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 | 4 | 2023 |

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 | 2 | 2024 |

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 | 2 | 2023 |

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

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 | 1 | 2024 |

Unbounded Separation Logic T Dardinier Archive of Formal Proofs, September, issn, 2022 | 1 | 2022 |

Beyond the frame rule: Static inlining in separation logic T Dardinier ETH Zurich, 2020 | 1 | 2020 |

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 |