BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Verified CompCert Front-End for a Memory Model supporting  Point
 er Arithmetic and Uninitialised Data - Sandrine Blazy\, University of Renn
 es 1
DTSTART:20160708T130000Z
DTEND:20160708T140000Z
UID:TALK65242@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:The CompCert C compiler guarantees that the target program beh
 aves as the source program. Yet\, source  programs without a defined seman
 tics do not benefit from this guarantee and could therefore be miscompiled
 .  To reduce the possibility of a miscompilation\, we propose a novel memo
 ry model for CompCert which gives a  defined semantics to challenging feat
 ures such as bitwise pointer arithmetics and access to uninitialised data.
 \n\nWe evaluate our memory model both theoretically and experimentally. In
  our experiments\, we identify pervasive low-level C idioms that require t
 he additional expressiveness provided by our memory model. We also show  t
 hat our memory model provably subsumes the existing CompCert memory model 
 thus cross-validating both semantics.\n \nOur memory model relies on the c
 ore concepts of symbolic value and normalisation. A symbolic value models 
 a delayed computation and the normalisation turns\, when possible\, a symb
 olic value into a genuine value.  We show how to tame the expressive power
  of the normalisation so that the memory model fits the proof framework of
  CompCert.  We also adapt the proofs of correctness of the compiler passes
  performed by CompCert’s front-end\, thus demonstrating that our model i
 s well-suited for  proving compiler transformations.
LOCATION:FW26
END:VEVENT
END:VCALENDAR