Colloquium Details
Sound and Automated Deductive Verifiers for Advanced Properties
Speaker: Thibault Dardinier, ETH Zurich
Location: 60 Fifth Avenue C15
Date: February 27, 2025, 2 p.m.
Host: Joe Tassarotti
Synopsis:
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.
Notes: In-person attendance only available to those with active NYU ID cards. Zoom alternatives are also available.
Speaker Bio:
Thibault Dardinier is a final-year PhD candidate at ETH Zurich, advised by Peter Müller. His research focuses on building provably sound deductive verifiers with state-of-the-art automation for correctness, security, and privacy properties. His work, regularly published in top conferences (POPL, PLDI, OOPSLA, CAV, IJCAR), has received multiple awards, including an ACM SIGPLAN Distinguished Paper Award and the ETH Zurich Medal. He has also won the annual VerifyThis verification competition multiple times. Before his PhD, he earned an MSc from ETH Zurich and a BSc from École Polytechnique in France. He has interned at Microsoft Research, SRI International, Siemens, and the French Ministry of Defense.