BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: Building systems that we can trust: compilers\, sem
 antics\, and tooling for end-to-end verified systems
DTSTART:20210318T140000
DTEND:20210318T150000
DTSTAMP:20260510T031408Z
UID:2b07ce6f4b5ae47f972995491860cc1dee6b925b3054bdcfd1526f8b
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Clément Pit-Claudel - MIT\nIC Faculty candidate\n\nAbstra
 ct\nComputer systems play a crucial role in our lives yet cannot be fully 
 trusted\, in part due to the persistence of software and hardware bugs.  
 Beyond costs and lost revenue\, these bugs put our privacy\, our well-bein
 g\, and sometimes even our lives at risk.\n\nWriting systems in high-level
  programming languages increases developer productivity and eliminates com
 mon sources of errors\, but compilers for these languages often produce re
 latively slow code.  As a result\, critical systems are still typically w
 ritten in low-level languages — and remain full of bugs.\n\nIn this talk
 \, I will discuss my efforts to build fast systems verified from end to en
 d\, starting from requirements formulated in high-level mathematical terms
  and deriving assembly code with uncompromising performance\, backed by ma
 chine-checked proofs of correctness.  The key component of this approach 
 is a new way of phrasing program compilation as an existentially quantifie
 d proof-search problem\; this enables users to customize their compilers a
 nd build systems in expressive languages without paying steep performance 
 penalties.\n\nThen\, because pure-software verification cannot protect aga
 inst hardware bugs\, I will describe my recent efforts to characterize the
  semantics of rule-based hardware-design languages and develop compilers\,
  verification technology\, and simulators for hardware systems.\n\nFinally
 \, as part of a vision to make verification and formal methods a standard 
 part of critical software and hardware development\, I will describe my ef
 forts to make verification work more approachable\, focusing on tools to h
 elp developers craft and comprehend mechanized proofs.\n\nBio\nClément Pi
 t-Claudel is a PhD candidate at MIT working in Adam Chlipala's lab.  He r
 eceived his BS and MSE at École Polytechnique in France and his MS at MIT
  in 2016.  His research focuses on programming languages\, extensible com
 pilers\, and verification\; his broader interests include systems engineer
 ing\, hardware design languages\, security\, optimization\, databases\, an
 d type theory.  Clément built the first end-to-end verified compilation 
 pipeline from high-level specifications to assembly language\, a fast simu
 lator and the first verified compiler for a rule-based hardware-design lan
 guage with EHRs\, and multiple widely-used tools for the Coq proof assista
 nt.  His application materials are at https://pit-claudel.fr/clement/facu
 lty-applications/\n\nMore information
LOCATION:https://epfl.zoom.us/j/89514399796?pwd=N3NFRW80NkFZVnd0Q3kwcEpvN2
 5JUT09
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR