Thibault Dardinier

PhD student, Programming Methodology Group, ETH Zurich
thibault.dardinier[at]inf.ethz.ch



About Publications Education Experience Awards Teaching Other Activities

About

I am a PhD student in the Programming Methodology Group at ETH Zurich, supervised by Prof. Peter Müller. My goal is to develop formal foundations (using the Isabelle proof assistant) for automatic deductive verifiers based on separation logic, with a particular focus on intermediate verification languages (such as Viper).

Before this, I graduated from ETH Zurich (as part of the Direct Doctorate program) and from École Polytechnique in France. During my studies, I completed internships at SRI International, Siemens, and the Ministry of Defense (France).

Publications

2022

Sound Automation of Magic Wands

Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers
Computer Aided Verification (CAV)
Abstract Link Extended version Slides Isabelle formalization (part 1) (part 2) Artifact

The magic wand −∗ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A footprint of a magic wand formula is a state that, combined with any state in which A holds, yields a state in which B holds. The key challenge of proving a magic wand (also called packaging a wand) is to find such a footprint. Existing package algorithms either have a high annotation overhead or, as we show in this paper, are unsound. We present a formal framework that precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics. We prove in Isabelle/HOL that our formal framework is sound and complete, and use it to develop a novel package algorithm that offers competitive automation and is sound. Moreover, we present a novel, restricted definition of wands and prove in Isabelle/HOL that it is possible to soundly combine fractions of such wands, which is not the case for arbitrary wands. We have implemented our techniques for the Viper language, and demonstrate that they are effective in practice.

2020

A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic

David Basin, Thibault Dardinier, Lukas Heimes, Srđan Krstić, Martin Raszyk, Joshua Schneider, Dmitriy Traytel
International Joint Conference on Automated Reasoning (IJCAR)
Abstract Link Isabelle formalization

Runtime monitors for rich specification languages are sophisticated algorithms, especially when they are heavily optimized. To gain trust in them and safely explore the space of possible optimizations, it is important to verify the monitors themselves. We describe the development and correctness proof in Isabelle/HOL of a monitor for metric first-order dynamic logic. This monitor significantly extends previous work on formally verified monitors by supporting aggregations, regular expressions (the dynamic part), and optimizations including multi-way joins adopted from databases and a new sliding window algorithm.

2020

Beyond the Frame Rule: Static Inlining in Separation Logic

Thibault Dardinier
Master's Thesis. ETH Zurich, Switzerland.
Abstract Link

Various formal verification techniques can be used to automatically verify the absence of errors in programs. This provides an advantage over testing approaches, namely the guarantee that a program is correct for any possible execution. However, such approaches often require a user to provide additional specifications to guide the verification, in the form of loop invariants and method preconditions and postconditions, which places a burden on the user. When no specifications are provided, verifiers usually report potential errors which are not actual errors, hence lowering confidence in error reporting. Users might want to learn quickly (without providing too many specifications) and with high confidence whether a program is incorrect. This would speed up the development and verification process by only having to provide specifications when one is fairly certain that the program is correct. Static inlining, that is inlining of method calls and unrolling of loop iterations, is an interesting approach to tackle this issue. Using approaches based on static inlining, verifiers could inform a user of the existence of fundamental errors, errors for which no annotation can make the program verify. The existence of fundamental errors indicates an error in the program itself, informing the user this program cannot be verified, without the user needing to waste time and energy in the search of the right annotation. One would expect that errors reported in an inlined program always correspond to fundamental errors in the original program, since annotations only serve as approximations of method calls and loops. Surprisingly, this is not always the case. Indeed, Viper, a verification infrastructure for permissionbased reasoning, partly based on separation logic and implicit dynamic frames with fractional permissions, has special features (such as permission introspection) which give rise to examples where this is not the case. These examples have all in common that they do not satisfy the frame rule. In this thesis, we find (and prove correct) a soundness condition which characterizes the set of Viper programs for which static inlining is sound, that is errors in the inlined program correspond to fundamental errors in the original program. We define a parametric language which generalizes Viper, where program states are elements of a separation algebra, define the soundness condition in terms of this language, and prove the soundness property of inlining under this soundness condition, using the proof assistant Isabelle/HOL. We then show how one can instantiate this parametric language to transfer the results to Viper. We also explore a completeness property of static inlining, and consider extensions to different loop semantics and different ways of inlining.

2018

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
Genetic and Evolutionary Computation Conference (GECCO)
Abstract Link

Evolutionary algorithms, being problem-independent and randomized heuristics, are generally believed to be robust to dynamic changes and noisy access to the problem instance. We propose a new method to obtain rigorous runtime results for such settings. In contrast to many previous works, our new approach mostly relies on general parameters of the dynamics or the noise models, such as the expected change of the dynamic optimum or the probability to have a dynamic change in one iteration. Consequently, we obtain bounds which are valid for large varieties of such models. Despite this generality, for almost all particular models regarded in the past our bounds are stronger than those given in previous works. As one particular result, we prove that the (1 + λ) EA can optimize the OneMax benchmark function efficiently despite a constant rate of 1-bit flip noise. For this, a logarithmic size offspring population suffices (the previous-best result required a super-linear value of λ). Our results suggest that the typical way to find the optimum in such adverse settings is not via a steady approach of the optimum, but rather via an exceptionally fast approach after waiting for a rare phase of low dynamic changes or noise.

Education

2018 - now

Direct Doctorate, ETH Zurich

Zurich, Switzerland The Direct Doctorate program combines a Master and a PhD in 5-6 years.
2018 - 20

Master of Computer Science with distinction, ETH Zurich, 5.8/6

Zurich, Switzerland
  • Part of the Direct Doctorate program.
  • Classes on theoretical computer science, formal verification, artificial intelligence and parallel computing.
  • Master's Thesis: Beyond the Frame Rule: Static Inlining in Separation Logic.
  • 2015 - 18

    Diplôme d'Ingénieur (MSc), École Polytechnique, 3.96/4 (top 5%)

    Palaiseau, France
  • Focus on Computer Science: Algorithms and Foundations of Programming Languages.
  • Minor: Mathematics, Applied Mathematics and Economy.
  • Member of the video association (JTX), the 2017 TEDx team, and player of the football team.
  • 2013 - 15

    Classes Préparatoires (MPSI-MP), Lycée du Parc

    Lyon, France
  • Two-year undergraduate preparatory course for the competitive entrance exams to France’s leading scientific schools.
  • Focus on Mathematics, Physics, Computer Science.
  • Admitted to École Polytechnique and ENS Paris (Ulm).
  • Experience

    2019 - 20

    Static Inlining in Separation Logic, ETH Zurich (Programming Methodology Group)

    Master's Thesis
    Supervision: Gaurav Parthasarathy, Prof. Peter Müller
    2019

    Formalizing Multiway-Join Algorithms in Isabelle/HOL, ETH Zurich (Information Security Group)

    Direct doctorate research project
    Supervision: Dr. Dmitriy Traytel, Martin Raszyk
  • Formalized and proved correct a generic multi-way join algorithm in Isabelle/HOL.
  • Integrated this algorithm in a formally verified monitor for metric first-order temporal, which led to better performance results.
  • Results published in IJCAR'20.
  • 2018

    Research Fellow, SRI International (CSL)

    Menlo Park, California, USA
    Supervision: Dr. Susmit Jha
  • Developed an extension of Gaussian Processes to symbolically reason over sets and trajectories in order to enable multiple-step ahead forecasting with propagation of uncertainty.
  • Received the Research Internship Prize from École Polytechnique.
  • 2017

    Theoretical Analysis of Evolutionary Algorithms, École Polytechnique (LIX)

    Supervision: Prof. Benjamin Doerr
  • Theoretical analysis of evolutionary algorithms for dynamic and noisy objectives.
  • Results published in GECCO'18
  • 2017

    R&D Intern, Siemens (Corporate Technology)

    Munich, Germany
  • Created a dynamic programming algorithm to locate a train without GPS, using other sensors and previous recordings, and filed an Invention Disclosure for this algorithm.
  • Enhanced an existing Indoor Positioning System Android app, based on Bluetooth Low Energy and Ultra-Wideband technologies.
  • Set a structure up on a server to collect data from the previous app in a database to run experiments and show the results.
  • 2015 - 16

    Research Intern, Ministry of Defense (France)

    Paris, France
  • Used ML methods to automate the processing and analysis of many documents (logistic regression, random forests).
  • Developed an app to interactively explore complex graphs.
  • Received the National Defense Medal.
  • Awards

    2022

    Best Overall Team, VerifyThis (Program Verification Competition)

    with Jonás Fiala
    • VerifyThis is a program verification competition, whose 2022 edition took place at ETAPS 2022 in Munich.
    • It offers several challenges presented in natural language and pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
    • Our team won the "Best Overall Team" prize using Viper.
    2020

    ETH Medal, ETH Zurich

    Awarded by ETH Zürich for my Master's thesis on inlining in separation logic, along with a financial sum. The ETH Medal is awarded to less than 2.5% of all Master's graduates of an ETH department.
    2018

    Research Internship Prize, École Polytechnique

    Awarded by École Polytechnique for my work on Gaussian Processes at SRI International.
    2016

    National Defense Medal (France)

    Awarded for my internship at the Ministry of Defense.
    2015

    3rd Place, Prologin (National Programming Contest)

    Prologin is a contest for French speaking students under 21, with qualifiers. The best 100 candidates meet and discover a multiplayer game created for the contest. They have 36 hours in a row to create an AI for the game. A ranking is established with the results of a contest between all AIs. Ranked 3rd.
    2014

    2nd Place, Prologin (National Programming Contest)

    Ranked 2nd.

    Teaching

    2020 - now

    Teaching Assistant, ETH Zurich

    Zurich, Switzerland
    2016 - 17

    Oral Examiner in Mathematics, Lycée Blaise Pascal

    Orsay, France
    Two hours weekly for undergraduates preparing competitive entrance exams to France’s top-ranking scientific schools.

    Other Activities

    2017

    Development of an Online Video Platform for the Video Association (JTX)

  • A YouTube-like website where the school video association shares its videos with the students, with many specific features.
  • Visited monthly by thousands students and alumni (restricted access for others).
  • 2017

    Development of an Optimization Algorithm (Bin Packing) for Industrial Purposes

  • Studied state-of-the-art algorithms to solve the “Bin packing” problem : Bin Completion (BC) by Korf [2002, 2003, 2013] and Branch-and-Cut-and-Price (BCP) by Belov and Scheithauer [2006].
  • Implemented an improved version of Korf’s BC algorithm.
  • Adapted the previous algorithm and other algorithms (such as Knapsack) to tackle industrial issues as requested.
  • 2016

    Volunteer, Mission Potosi

    Potosi, Bolivia
    Mission Potosi is an organisation with about 50 students from 4 schools (business, medical and engineering), which collaborates with local ONGs (Cepromin, Pasocap) and a german ONG (Kindernothilfe) in Potosi (Bolivia) to provide childcare for mining families.
  • Helped to develop and maintain a children's center.
  • Helped children with school and sanitary issues.
  • Collected money to give deserving children scholarships.
  • 2015

    Military Training as an Officer

    Coëtquidan, France
    This military training, part of the cursus at École polytechnique, teaches us a lot on various subjects such as strategy, communication, leadership, etc.