Thibault Dardinier

Dr. Thibault Dardinier is currently a Postdoctoral Researcher at EPFL, where he works with Nate Foster, and will join the Courant Institute of Mathematical Sciences at New York University as an Assistant Professor of Computer Science in Fall 2026, as part of the Analysis of Computer Systems group. His research focuses on building provably sound deductive program verifiers with state-of-the-art automation for correctness, security, and privacy properties. His work bridges theory and practice in formal methods, spanning the development of machine-checked program logics (using the Isabelle proof assistant) and the design of novel automated verification tools. He has contributed foundational results in areas such as Hyper Hoare Logic, concurrent separation logic, information-flow security, and verification-preserving translations, and has built practical verifiers such as Hypra. His research has been published at leading venues including PLDI, POPL, and OOPSLA. Dr. Dardinier received his Ph.D. from ETH Zurich under the supervision of Peter Müller, and previously held a visiting research fellowship at the National University of Singapore with Ilya Sergey. He has also completed an internship at Microsoft Research. He plans to recruit two Ph.D. students starting in September 2026 at NYU and welcomes applications from students interested in program verification, formal reasoning, and secure systems.