BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Vellvm: Formal Verification of LLVM IR Code
DTSTART:20260506T100000
DTEND:20260506T110000
DTSTAMP:20260531T222112Z
UID:fd4211380af6c0b38e337158f129def788be736bfb64093905d3e811
CATEGORIES:Conferences - Seminars
DESCRIPTION:By. Dr. Steve Zdancewic\n\nAbstract\nLLVM is an industrial-st
 rength compiler that's used for everything from iOS development to academi
 c research.  However\, like any piece of complicated software\, LLVM IR i
 tself has a complex specification\, making it hard to fully understand\, a
 nd its implementation has bugs\, which can cause potentially catastrophic 
 mis-compilation errors. These properties make the LLVM framework a sweet s
 pot for bug-finding and verification technologies--any improvements to it 
 are amplified across its many applications.\n\nThis talk will survey the V
 ellvm (Verified LLVM) project\, which aims to define a formal\, mathematic
 al specification for a large\, useful subset of LLVM.  Vellvm is implemen
 ted in the Rocq interactive theorem prover\, which can be used for develop
 ing machine-checkable properties about LLVM IR programs and compiler optim
 ization passes.  Along the way\, we'll explore some subtleties of LLVM IR
  semantics and see how Vellvm models them in a modular way by composing "m
 onadic interpreters" built on top of a data structure called _interaction 
 trees_. We'll also see some applications of Vellvm for verified compiler c
 onstruction.\n\nBio\nDr. Zdancewic is the Schlein Family President's Disti
 nguished Professor in the Computer and Information Science Department at t
 he University of Pennsylvania. He received his Ph.D. in Computer Science f
 rom Cornell University in 2002\, and he graduated from Carnegie Mellon Uni
 versity with a B.S. in Computer Science and Mathematics in 1996.  He is t
 he recipient of an NSF Graduate Research Fellowship\, an Intel fellowship\
 , an NSF CAREER award\, and a Sloan Fellowship. His numerous publications 
 in the areas of programming languages and computer security include severa
 l best paper awards.\n\nMore information\n\nRecording\n 
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/65703840090
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR