BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified Software Toolchains:  Foundational verification of C prog
 rams using VST - Lennart Beringer (Princeton University)
DTSTART:20220713T101500Z
DTEND:20220713T110000Z
UID:TALK176246@talks.cam.ac.uk
DESCRIPTION:The Verified Software Toolchain (VST) is a verification tool i
 n Coq for establishing functional correctness of C programs with respect t
 o specifications expressed in a higher-order concurrent separation logic\,
  and with a mechanized soundness proof that connects to the operational se
 mantics of CompCert Clight.&nbsp\; The presentation will survey existing a
 nd ongoing applications of VST to code bases from a range of domains\, pay
 ing particular attention to its ability to the bridge abstraction gap betw
 een program verification model-level reasoning.\n&nbsp\;
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR