BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Optimizations in a formally verified compiler - David Monniaux\, C
 NRS/VERIMAG and École Polytechnique
DTSTART:20230720T130000Z
DTEND:20230720T140000Z
UID:TALK203299@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:CompCert is a formally verified compiler. "Formally verified"\
 nmeans that there is a mathematical proof that the execution of the\nsourc
 e matches that of the assembly code\, and this proof has been\nchecked by 
 a proof assistant (here\, Coq).\nIt however provided limited optimization.
  We have since then\nimplemented a variety of optimizations (scheduling\, 
 strength reduction\nacross loop iterations…) that significantly reduce t
 he gap compared to\nGCC. We also implemented a back-end for the Kalray KVX
  VLIW manycore  processor.\nI will discuss these optimizations\, as well a
 s our plans for security  features and Rust compilation.\n\nBio: David Mon
 niaux obtained his PhD in 2001 in Paris under Prof Patrick Cousot\; his di
 ssertation was on the static analysis of probabilistic programs by abstrac
 t interpretation. He then joined CNRS as a junior researcher and first wor
 ked on the Astrée static analyzer\, still in Paris. In 2007 he transferre
 d to VERIMAG in Grenoble\, where he works on various aspects of program ve
 rification (decision procedures\, abstract interpretation…). He now is a
  senior researcher at CNRS and an adjunct professor at École polytechniqu
 e.
LOCATION:FW11\, Computer Laboratory
END:VEVENT
END:VCALENDAR