BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Sound and Automated Deductive Verifiers for Advance
 d Properties
DTSTART:20250310T101500
DTEND:20250310T111500
DTSTAMP:20260430T171424Z
UID:27c6f469feae8bab238ff605da6926dd9a8226540cd0f952a690141f
CATEGORIES:Conferences - Seminars
DESCRIPTION:By : Thibault Dardinier - ETH Zurich\nIC Faculty candidate\n\n
 Abstract\nAutomated deductive verifiers are tools that take as input a pro
 gram and a specification and attempt to construct a formal proof\, using a
  program logic\, that the program satisfies its specification. Modern veri
 fiers have had significant practical impact\, with notable examples includ
 ing the use of Dafny at Amazon\, F* at Microsoft\, and Viper in the Verifi
 edSCION project. However\, modern verifiers face two fundamental challenge
 s: trustworthiness (how can we ensure that verifiers are sound?) and expre
 ssivity (how can we build verifiers that can prove security and privacy pr
 operties?).\n\nIn this talk\, I will present my research\, which addresses
  both challenges. First\, I will discuss a formal framework for proving th
 e soundness of modern verifiers based on separation logic (a state-of-the-
 art program logic for modular reasoning about sequential and concurrent pr
 ograms). Second\, I will present an expressive program logic for hyperprop
 erties (properties relating multiple executions of a program)\, which has 
 been automated in a deductive verifier. Finally\, I will outline my resear
 ch agenda for developing trustworthy\, automated verifiers for advanced co
 rrectness and security properties.\n\nBio\nThibault Dardinier is a final-y
 ear PhD candidate at ETH Zurich\, advised by Peter Müller. His research f
 ocuses on building provably sound deductive verifiers with state-of-the-ar
 t automation for correctness\, security\, and privacy properties. His work
 \, regularly published in top conferences (POPL\, PLDI\, OOPSLA\, CAV\, IJ
 CAR)\, has received multiple awards\, including an ACM SIGPLAN Distinguish
 ed Paper Award and the ETH Zurich Medal. He has also won the annual Verify
 This verification competition multiple times. Before his PhD\, he earned a
 n MSc from ETH Zurich and a BSc from École Polytechnique. He has interned
  at Microsoft Research\, SRI International\, Siemens\, and the French Mini
 stry of Defense.\n\nMore information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/68278906185
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR