Thibault Dardinier

PhD student, Programming Methodology Group, ETH Zurich
firstname.lastname@inf.ethz.ch


About Publications Talks Education Awards Internships Supervision Teaching Service Other

About

I am a PhD student in the Programming Methodology Group at ETH Zurich, supervised by Prof. Peter Müller. My main 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). I am also interested in developing techniques and tools to prove that programs satisfy hyperproperties (properties relating multiple executions of the same program).

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

Publications

Conference

2025
POPL

Formal Foundations for Translational Separation Logic Verifiers

Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller ACM SIGPLAN Symposium on Principles of Programming Languages
[Abstract] [PDF] [Publisher]

Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3. The resulting IVL program is then verified using an existing back-end verifier. A soundness proof for such a translational verifier needs to relate the input program and verification logic to the semantics of the IVL, which in turn needs to be connected with the verification logic implemented in the back-end verifiers. Performing such proofs is challenging due to the large semantic gap between the input and output programs and logics, especially for complex verification logics such as separation logic. This paper presents a formal framework for reasoning about translational separation logic verifiers. At its center is a generic core IVL that captures the essence of different separation logics. We define its operational semantics and formally connect it to two different back-end verifiers, which use symbolic execution and verification condition generation, resp. Crucially, this semantics uses angelic non-determinism to enable the application of different proof search algorithms and heuristics in the back-end verifiers. An axiomatic semantics for the core IVL simplifies reasoning about the front-end translation by performing essential proof steps once and for all in the equivalence proof with the operational semantics rather than for each concrete front-end translation. We illustrate the usefulness of our formal framework by instantiating our core IVL with elements of Viper and connecting it to two Viper back-ends as well as a front-end for concurrent separation logic. All our technical results have been formalized in Isabelle/HOL, including the core IVL and its semantics, the semantics of two back-ends for a subset of Viper, and all proofs.

2024
OOPSLA

Hypra: A Deductive Program Verifier for Hyper Hoare Logic

Thibault Dardinier*, Anqi Li*, Peter Müller ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
[Abstract] [PDF] [Publisher] [Artifact]

Hyperproperties relate multiple executions of a program and are useful to express common correctness properties (such as determinism) and security properties (such as non-interference). While there are a number of powerful program logics for the deductive verification of hyperproperties, their automation falls behind. Most existing deductive verification tools are limited to safety properties, but cannot reason about the existence of executions, for instance, to prove the violation of a safety property. Others support more flexible hyperproperties such as generalized non-interference, but have limitations in terms of the programs and proof structures they support. In this paper, we present the first deductive verification technique for arbitrary hyperproperties over multiple executions of the same program. Our technique automates the generation of verification conditions for Hyper Hoare Logic. Our key insight is that arbitrary hyperproperties and the corresponding proof rules can be encoded into a standard intermediate verification language by representing sets of states of the input program explicitly in the states of the intermediate program. Verification is then automated using an existing SMT-based verifier for the intermediate language. We implement our technique in a tool called Hypra and demonstrate that it can reliably verify complex hyperproperties.

PLDI

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties

Thibault Dardinier, Peter Müller ACM SIGPLAN International Conference on Programming Language Design and Implementation
[Abstract] [PDF] [Publisher] [Extended version] [Artifact] [Archive of Formal Proofs]

Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (so-called trace properties, such as functional correctness). Hoare logic has been generalized to prove also properties of multiple executions of a program (so-called hyperproperties, such as determinism or non-interference). These program logics prove the absence of (bad combinations of) executions. On the other hand, program logics similar to Hoare logic have been proposed to disprove program properties (e.g., Incorrectness Logic), by proving the existence of (bad combinations of) executions. All of these logics have in common that they specify program properties using assertions over a fixed number of states, for instance, a single pre- and post-state for functional properties or pairs of pre- and post-states for non-interference. In this paper, we present Hyper Hoare Logic, a generalization of Hoare logic that lifts assertions to properties of arbitrary sets of states. The resulting logic is simple yet expressive: its judgments can express arbitrary trace- and hyperproperties over the terminating executions of a program. By allowing assertions to reason about sets of states, Hyper Hoare Logic can reason about both the absence and the existence of (combinations of) executions, and, thereby, supports both proving and disproving program (hyper-)properties within the same logic, including (hyper-)properties that no existing Hoare logic can express. We prove that Hyper Hoare Logic is sound and complete, and demonstrate that it captures important proof principles naturally. All our technical results have been proved in Isabelle/HOL.

PLDI

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language

Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers ACM SIGPLAN International Conference on Programming Language Design and Implementation
[Abstract] [PDF] [Publisher] [Extended version] [Artifact]

Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end generates proof obligations for the IVL program and employs an SMT solver to discharge them. Soundness of such verifiers therefore requires that the front-end translation faithfully captures the semantics of the input program and specification in the IVL program, and that the back-end reports success only if the IVL program is actually correct. For a verification tool to be trustworthy, these soundness conditions must be satisfied by its actual implementation, not just the program logic it uses. In this paper, we present a novel validation methodology that provides formal soundness guarantees for front-end implementations. For each successful run of the verifier, we automatically generate a proof in Isabelle showing that the correctness of the produced IVL program implies the correctness of the input program. This proof can be checked independently from the verifier in Isabelle and can be combined with existing work on validating back-ends to obtain an end-to-end soundness guarantee. Our methodology based on forward simulation employs several modularisation strategies to handle the large semantic gap between the input language and the IVL, as well as the intricacies of practical, optimised translations. We present our methodology for the widely-used Viper and Boogie languages. Our evaluation demonstrates that it is effective in validating the translations performed by the existing Viper implementation.

2023
PLDI

CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity

Marco Eilers, Thibault Dardinier, Peter Müller ACM SIGPLAN International Conference on Programming Language Design and Implementation
[Abstract] [PDF] [Publisher] [Extended version] [Artifact] [Archive of Formal Proofs]

Information flow security ensures that the secret data manipulated by a program does not influence its observable output. Proving information flow security is especially challenging for concurrent programs, where operations on secret data may influence the execution time of a thread and, thereby, the interleaving between different threads. Such internal timing channels may affect the observable outcome of a program even if an attacker does not observe execution times. Existing verification techniques for information flow security in concurrent programs attempt to prove that secret data does not influence the relative timing of threads. However, these techniques are often restrictive (for instance because they disallow branching on secret data) and make strong assumptions about the execution platform (ignoring caching, processor instructions with data-dependent runtime, and other common features that affect execution time). In this paper, we present a novel verification technique for secure information flow in concurrent programs that lifts these restrictions and does not make any assumptions about timing behavior. The key idea is to prove that all mutating operations performed on shared data commute, such that different thread interleavings do not influence its final value. Crucially, commutativity is required only for an abstraction of the shared data that contains the information that will be leaked to a public output. Abstract commutativity is satisfied by many more operations than standard commutativity, which makes our technique widely applicable. We formalize our technique in CommCSL, a relational concurrent separation logic with support for commutativity-based reasoning, and prove its soundness in Isabelle/HOL. We implemented CommCSL in HyperViper, an automated verifier based on the Viper verification infrastructure, and demonstrate its ability to verify challenging examples.

OOPSLA

Verification-Preserving Inlining in Automatic Separation Logic Verifiers

Thibault Dardinier, Gaurav Parthasarathy, Peter Müller ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
[Abstract] [PDF] [Publisher] [Extended version] [Artifact]

Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (bounded) inlining and about loops via (bounded) unrolling does not require method specifications and loop invariants and, therefore, reduces the annotation overhead to the bare minimum, namely specifications of the properties to be verified. For verifiers based on traditional program logics, verification via inlining (and unrolling) is verification-preserving: successful unbounded verification of a program w.r.t. some annotation implies successful verification of the inlined program. That is, any error detected in the inlined program reveals a true error in the original program. However, this essential property might not hold for automatic separation logic verifiers such as Caper, GRASShopper, RefinedC, Steel, VeriFast, and verifiers based on Viper. In this setting, inlining generally changes the resources owned by method executions, which may affect automatic proof search algorithms and introduce spurious errors. In this paper, we present the first technique for verification-preserving inlining in automatic separation logic verifiers. We identify a semantic condition on programs and prove in Isabelle/HOL that it ensures verification-preserving inlining for state-of-the-art automatic separation logic verifiers. We also prove a dual result: successful verification of the inlined program ensures that there are method and loop annotations that enable the verification of the original program for bounded executions. To check our semantic condition automatically, we present two approximations that can be checked syntactically and with a program verifier, respectively. We implement these checks in Viper and demonstrate that they are effective for non-trivial examples from different verifiers.

2022
OOPSLA

Fractional Resources in Unbounded Separation Logic

Thibault Dardinier, Peter Müller, Alexander J. Summers ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
[Abstract] [PDF] [Publisher] [Slides] [Artifact] [Archive of Formal Proof]

MedalACM SIGPLAN Distinguished Paper Award

Many separation logics support fractional permissions to distinguish between read and write access to a heap location, for instance, to allow concurrent reads while enforcing exclusive writes. Fractional permissions extend to composite assertions such as (co)inductive predicates and magic wands by allowing those to be multiplied by a fraction. Typical separation logic proofs require that this multiplication has three key properties: it needs to distribute over assertions, it should permit fractions to be factored out from assertions, and two fractions of the same assertion should be combinable into one larger fraction. Existing formal semantics incorporating fractional assertions into a separation logic define multiplication semantically (via models), resulting in a semantics in which distributivity and combinability do not hold for key resource assertions such as magic wands, and fractions cannot be factored out from a separating conjunction. By contrast, existing automatic separation logic verifiers define multiplication syntactically, resulting in a different semantics for which it is unknown whether distributivity and combinability hold for all assertions. In this paper, we present a novel semantics for separation logic assertions that allows states to hold more than a full permission to a heap location during the evaluation of an assertion. By reimposing upper bounds on the permissions held per location at statement boundaries, we retain key properties of separation logic, in particular, the frame rule. Our assertion semantics unifies semantic and syntactic multiplication and thereby reconciles the discrepancy between separation logic theory and tools and enjoys distributivity, factorisability, and combinability. We have formalised our semantics and proved its properties in Isabelle/HOL.

CAV

Sound Automation of Magic Wands

Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers International Conference on Computer Aided Verification
[Abstract] [PDF] [Publisher] [Extended version] [Slides] [Artifact] [Archive of Formal Proof]

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.

ICTAC
(invited)

VeriMon: A Formally Verified Monitoring Tool

David Basin, Thibault Dardinier, Nico Hauser, Lukas Heimes, Jonathan Julián Huerta y Munive, Nicolas Kaletsch, Srđan Krstić, Emanuele Marsicano, Martin Raszyk, Joshua Schneider, Dawit Legesse Tirore, Dmitriy Traytel, Sheila Zingg International Colloquium on Theoretical Aspects of Computing
[Abstract] [PDF] [Publisher]

A runtime monitor observes a running system and checks whether the sequence of events the system generates satisfies a given specification. We describe the evolution of VeriMon: an expressive and efficient monitor that has been formally verified using the Isabelle proof assistant.

2020
IJCAR

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
[Abstract] [PDF] [Publisher] [Archive of Formal Proof]

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.

2018
GECCO

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
[Abstract] [PDF] [Publisher]

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.

Master's Thesis

2020

Beyond the Frame Rule: Static Inlining in Separation Logic

Thibault Dardinier
Master's Thesis. ETH Zurich, Switzerland.
[Abstract] [PDF]

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.

MedalETH Medal for Outstanding Master's Thesis

Talks

June 2024

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties

Conference talk at PLDI 2024
[Abstract] [Recording] [Paper]

Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (so-called trace properties, such as functional correctness). Hoare logic has been generalized to prove also properties of multiple executions of a program (so-called hyperproperties, such as determinism or non-interference). These program logics prove the absence of (bad combinations of) executions. On the other hand, program logics similar to Hoare logic have been proposed to disprove program properties (e.g., Incorrectness Logic), by proving the existence of (bad combinations of) executions. All of these logics have in common that they specify program properties using assertions over a fixed number of states, for instance, a single pre- and post-state for functional properties or pairs of pre- and post-states for non-interference. In this paper, we present Hyper Hoare Logic, a generalization of Hoare logic that lifts assertions to properties of arbitrary sets of states. The resulting logic is simple yet expressive: its judgments can express arbitrary trace- and hyperproperties over the terminating executions of a program. By allowing assertions to reason about sets of states, Hyper Hoare Logic can reason about both the absence and the existence of (combinations of) executions, and, thereby, supports both proving and disproving program (hyper-)properties within the same logic, including (hyper-)properties that no existing Hoare logic can express. We prove that Hyper Hoare Logic is sound and complete, and demonstrate that it captures important proof principles naturally. All our technical results have been proved in Isabelle/HOL.

January 2024

Formal Foundations of the Viper Verification Infrastructure

Workshop talk at the Swiss Verification Day 2024
[Abstract] [Slides]

The Viper verification infrastructure provides an architecture on which new automatic verification tools and prototypes can be developed simply and quickly. Viper comprises an intermediate verification language (the Viper language) based on separation logic, as well as automatic verifiers for the language. In this talk, I will first give an overview of Viper. I will then present and illustrate the use of inhale and exhale, two key verification primitives provided by Viper. Finally, I will describe our ongoing work to give formal foundations to Viper, which includes proving that the successful verification of a Viper program corresponds to a valid proof in separation logic.

October 2023

Verification-Preserving Inlining in Automatic Separation Logic Verifiers

Conference talk at OOPSLA 2023
[Abstract] [Recording] [Paper]

Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (bounded) inlining and about loops via (bounded) unrolling does not require method specifications and loop invariants and, therefore, reduces the annotation overhead to the bare minimum, namely specifications of the properties to be verified. For verifiers based on traditional program logics, verification via inlining (and unrolling) is verification-preserving: successful unbounded verification of a program w.r.t. some annotation implies successful verification of the inlined program. That is, any error detected in the inlined program reveals a true error in the original program. However, this essential property might not hold for automatic separation logic verifiers such as Caper, GRASShopper, RefinedC, Steel, VeriFast, and verifiers based on Viper. In this setting, inlining generally changes the resources owned by method executions, which may affect automatic proof search algorithms and introduce spurious errors. In this paper, we present the first technique for verification-preserving inlining in automatic separation logic verifiers. We identify a semantic condition on programs and prove in Isabelle/HOL that it ensures verification-preserving inlining for state-of-the-art automatic separation logic verifiers. We also prove a dual result: successful verification of the inlined program ensures that there are method and loop annotations that enable the verification of the original program for bounded executions. To check our semantic condition automatically, we present two approximations that can be checked syntactically and with a program verifier, respectively. We implement these checks in Viper and demonstrate that they are effective for non-trivial examples from different verifiers.

September 2023

Intuitive and Automated Reasoning for Concurrent Programs in Pulse

End of internship talk at Microsoft Research (Redmond)
May 2023

Viper: A Verification Framework Designed to Automate Separation Logic

Invited talk at the Iris Workshop 2023
[Abstract] [Slides]

Viper is a framework on which new automatic verification tools and prototypes can be developed simply and quickly. Viper comprises an intermediate verification language (the Viper language) based on separation logic, as well as automatic verifiers for the language. In this talk, I will first give an overview of Viper. I will then discuss how the design of the Viper language enables automatic verification. Finally, I will describe our ongoing work to give a formal foundation for Viper, which includes proving that the successful verification of a Viper program corresponds to a valid proof in separation logic.

May 2023

Proving Information Flow Security for Concurrent Programs

Invited talk at the Zurich Information Security and Privacy Center (ZISC) Seminar
[Abstract] [Slides] [Paper]

(Program) verification is the process of proving that a program satisfies some properties by using mathematical techniques and formal reasoning, rather than relying on testing the program with inputs. Program verification is typically used to prove functional correctness properties (e.g., proving that a sorting algorithm does not crash and correctly sorts inputs), but it can also be used to prove security properties such as information flow security, which ensures that the secret data manipulated by a program does not influence its observable output. Proving information flow security is especially challenging for concurrent programs, where operations on secret data may influence the execution time of a thread and, thereby, the interleaving between different threads. Such internal timing channels may affect the observable outcome of a program even if an attacker does not observe execution times. Existing verification techniques for information flow security in concurrent programs attempt to prove that secret data does not influence the relative timing of threads. However, these techniques are often restrictive (for instance because they disallow branching on secret data) and make strong assumptions about the execution platform (ignoring caching, processor instructions with data-dependent runtime, and other common features that affect execution time). In this talk, we present a novel verification technique for secure information flow in concurrent programs that lifts these restrictions and does not make any assumptions about timing behavior. The key idea is to prove that all mutating operations performed on shared data commute, such that different thread interleavings do not influence its final value. Crucially, commutativity is required only for an abstraction of the shared data that contains the information that will be leaked to a public output. Abstract commutativity is satisfied by many more operations than standard commutativity, which makes our technique widely applicable. We formalize our technique in CommCSL, a relational concurrent separation logic with support for commutativity-based reasoning, and prove its soundness in Isabelle/HOL. We implemented CommCSL in HyperViper, an automated verifier based on the Viper verification infrastructure, and demonstrate its ability to verify challenging examples.

December 2022

Fractional Resources in Unbounded Separation Logic

Conference talk at OOPSLA 2022
[Abstract] [Slides] [Recording] [Paper]

Many separation logics support fractional permissions to distinguish between read and write access to a heap location, for instance, to allow concurrent reads while enforcing exclusive writes. Fractional permissions extend to composite assertions such as (co)inductive predicates and magic wands by allowing those to be multiplied by a fraction. Typical separation logic proofs require that this multiplication has three key properties: it needs to distribute over assertions, it should permit fractions to be factored out from assertions, and two fractions of the same assertion should be combinable into one larger fraction. Existing formal semantics incorporating fractional assertions into a separation logic define multiplication semantically (via models), resulting in a semantics in which distributivity and combinability do not hold for key resource assertions such as magic wands, and fractions cannot be factored out from a separating conjunction. By contrast, existing automatic separation logic verifiers define multiplication syntactically, resulting in a different semantics for which it is unknown whether distributivity and combinability hold for all assertions. In this paper, we present a novel semantics for separation logic assertions that allows states to hold more than a full permission to a heap location during the evaluation of an assertion. By reimposing upper bounds on the permissions held per location at statement boundaries, we retain key properties of separation logic, in particular, the frame rule. Our assertion semantics unifies semantic and syntactic multiplication and thereby reconciles the discrepancy between separation logic theory and tools and enjoys distributivity, factorisability, and combinability. We have formalised our semantics and proved its properties in Isabelle/HOL.

August 2022

Sound Automation of Magic Wands

Conference talk at CAV 2022
[Abstract] [Slides] [Paper]

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.

Education

2020 - now

PhD Student, ETH Zurich

Zurich, Switzerland Part of the Direct Doctorate program.
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.
  • Received the ETH Medal for my 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).
  • Awards

    2024

    Best Student Team, VerifyThis (Program Verification Competition)

    with Jonás Fiala
    • VerifyThis is a program verification competition, which takes yearly place during ETAPS.
    • 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 Student Team" prize using Viper.
    2023

    Best Student Team, VerifyThis (Program Verification Competition)

    with Jonás Fiala Our team won the "Best Student Team" prize using Viper.
    2022

    ACM SIGPLAN Distinguished Paper Award (OOPSLA)

    For the paper Fractional Resources in Unbounded Separation Logic.

    Best Overall Team, VerifyThis (Program Verification Competition)

    with Jonás Fiala
    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.

    Internships

    2023

    Research Intern, Microsoft Research (RiSE)

    Redmond, Washington, USA
    Supervision: Guido Martinez, Tahina Ramananandro, Nikhil Swamy
    Worked on Pulse, a novel DSL built within the F* proof assistant, which offers both a language to write imperative concurrent programs in a Rust-like syntax and a checker based on concurrent separation logic to verify programs written in this DSL (with the help of proof annotations from the user). In particular, I developed a new way to automatically infer suitable annotations for parallel programs, reducing the proof burden on the user. I also worked on a new intuitive way of specifying and proving properties that will hold in the future (e.g., when a task will be done).
    2018

    Research Fellow, SRI International (CSL)

    Menlo Park, California, USA
    Supervision: 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

    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 machine learning methods to automate the processing and analysis of many documents.
  • Developed an app to interactively explore complex graphs.
  • Received the National Defense Medal.
  • Student Supervision

    Ongoing Yushuo Xiao (MSc thesis, co-supervised with Gaurav Parthasarathy)
    Foundational Proofs for Automated Verifiers with Separation Logic Predicates (project description)
    Trayan Gospodinov (MSc thesis)
    Hyper Separation Logic: (Dis-)Proving Hyperproperties of Programs with Pointers (project description)
    2024 Hongyi Ling (MSc thesis, co-supervised with Gaurav Parthasarathy)
    A General Approach to Formally Verify Viper Front-ends
    Yushuo Xiao (MSc practical work project)
    Hyperwand: Extending the Magic Wand Operator in Separation Logic (project description)
    Yiqun Liu (MSc practical work project)
    Automating Magic Wands with Advanced Features (project description)
    Hongyi Ling (MSc practical work project, co-supervised with Gaurav Parthasarathy)
    Formally Deriving an Equirecursive Viper Semantics via a Least Fixed Point Predicate Interpretation (project description)
    Ellen Arlt (MSc thesis, co-supervised with Gaurav Parthasarathy)
    A Formally Verified Automatic Verifier for Concurrent Programs
    Anqi Li (MSc practical work project)
    Improving User-Defined Permission Models in Viper
    Dina Weiersmüller (BSc thesis, co-supervised with Linard Arquint)
    Advanced Logical Proofs in a Verifier
    2022 Matthias Schenk (BSc thesis)
    Practical Inlining in Viper
    Nicola Widmer (BSc thesis, co-supervised with Malte Schwerhoff)
    Sound Automation of Magic Wands in a Symbolic-Execution Verifier
    Noé Weeks (BSc internship, co-supervised with Gaurav Parthasarathy)
    Making Magic Wands Combinable
    Benjamin Bonneau (MSc internship, co-supervised with Gaurav Parthasarathy)
    A Formal Foundation for the Dafny Verifier

    Teaching

    2020 - now

    Teaching Assistant, ETH Zurich

    Zurich, Switzerland
    2021 - 2022

    Head Teaching Assistant, ETH Zurich

    Zurich, Switzerland
    Formal Methods and Functional Programming (2021 and 2022)
    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.

    Service

    Subreviewer PLDI'22, TACAS'23, POPL'24, LICS'24
    External reviewer POPL'24
    Student volunteer POPL'24

    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).
  • 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.