BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:How to provide proof that software is bug-free? Verified compilati
 on to the rescue
DTSTART:20240227T111500
DTEND:20240227T121500
DTSTAMP:20260510T043017Z
UID:b37f508d8ae71024ef9d4f5febbbfd860e98234e8a23a3fa612e5ed2
CATEGORIES:Conferences - Seminars
DESCRIPTION:Professor Sandrine Blazy (IRISA)\nDeductive verification provi
 des very strong guarantees that software is bug-free. Since the verificati
 on is usually done at the source level\, the compiler becomes a weak link 
 in the software-production chain. Verifying the compiler itself provides g
 uarantees that no errors are introduced during compilation. This talk will
  illustrate this approach through CompCert\, the first fully verified comp
 iler for C that is actually usable on real source code and that produces d
 ecent target code on real-world architectures. More generally\, this appro
 ach opens the way to the verification of software tools involved in the pr
 oduction and verification of software
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR