Talk: Sound and Automated Deductive Verifiers for Advanced Properties

LIVE STREAM: https://uwmadison.zoom.us/j/92829687761?pwd=96pakDtvmilcNrlRng9aNpiavvbiwr.1

Abstract: Automated deductive verifiers are tools that take as input a program and a specification and attempt to construct a formal proof, using a program logic, that the program satisfies its specification. Modern verifiers have had significant practical impact, with notable examples including the use of Dafny at Amazon, F* at Microsoft, and Viper in the VerifiedSCION project. However, modern verifiers face two fundamental challenges: trustworthiness (how can we ensure that verifiers are sound?) and expressivity (how can we build verifiers that can prove security and privacy properties?).

In this talk, I will present my research, which addresses both challenges. First, I will introduce a comprehensive formal framework for systematically proving the soundness of modern verifiers based on separation logic (a state-of-the-art program logic for modular reasoning about sequential and concurrent programs). Second, I will present an expressive program logic for hyperproperties (properties relating multiple executions of a program), which has been automated in a deductive verifier. Finally, I will outline my research agenda for developing trustworthy, automated verifiers for advanced correctness and security properties.

Bio: Thibault Dardinier is a PhD student in the Programming Methodology Group at ETH Zurich, advised by Prof. Peter Müller. The goal of his research is to build provably sound deductive verifiers with state-of-the-art automation for correctness, security, and privacy properties. To achieve this goal, his research addresses both theoretical and practical aspects, ranging from developing machine-checked program logics (e.g., Hyper Hoare Logic or CommCSL) and formal foundations (e.g., for translational verifiers based on separation logic, magic wands, fractional resources, or verification-preserving inlining) to building novel automated verifiers (e.g., Hypra).

During his PhD, Thibault completed an internship at Microsoft Research. Before his PhD, he graduated from ETH Zurich (as part of the Direct Doctorate program) and from École Polytechnique in France, and completed internships at SRI International, Siemens, and the Ministry of Defense (France).  Thibault received a Distinguished Paper Award at OOPSLA 2022 and the ETH Medal in 2020 for his MSc. thesis.