BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cerberus C semantics &amp\; pointer provenance  - Kayvan Memarian 
 (University of Cambridge)
DTSTART:20200228T130000Z
DTEND:20200228T140000Z
UID:TALK140419@talks.cam.ac.uk
CONTACT:Jean Pichon-Pharabod
DESCRIPTION:The C programming language is notionally defined by an ISO sta
 ndard\, the "de facto" usage of the language has however diverged over tim
 e from the standard semantics. The main point of disagreement concerns the
  memory object model\, and in particular the semantics of pointers. While 
 system programmers often rely on a very concrete view of pointers (sometim
 es even more concrete than what the ISO standard describes)\, compiler imp
 lementers take a more abstract view. Some compiler optimisations\, in part
 icular the ones based on alias analysis\, reason about how pointer values 
 are constructed during the program execution instead of only considering t
 heir representation.\n\nIn this talk\, I will present a source-language se
 mantics for pointer values and memory operations formalising a notion of p
 rovenance. It aims at reconciling the concrete and abstract views of the C
  memory model.\n\nThis work is part of the Cerberus project\, an executabl
 e semantics for a substantial fragment of C\, which I will also present. I
 n this model\, we define the semantics of C by elaboration into a Core int
 ermediate language where we make much of the language subtleties syntactic
 ally explicit\, while at the same time keeping some level of implementatio
 n agnosticism. Being executable\, Cerberus can be used as an oracle for ex
 ploring the range of behaviours that one should expect for reasonably size
 d programs.\n\nMore information\, including a link to Cerberus' web interf
 ace\, is available at\nhttps://www.cl.cam.ac.uk/~pes20/cerberus
LOCATION:Computer Laboratory\, room SS03
END:VEVENT
END:VCALENDAR