Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

New for: D1, D2, D3, D4, D5
<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:The C standard formalized in Coq
Speaker:Robbert Krebbers
coming from:Aarhus University
Speakers Bio:
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Expert Audience
Date, Time and Location
Date:Tuesday, 15 December 2015
Duration:60 Minutes
Building:E1 5
In my PhD thesis I have developed a formal semantics of a significant
part of the C programming language as described by the C11 standard.
In this talk I will give a brief overview of the main parts of my
formalized semantics.

* A structured memory model based on trees to capture subtleties of
C11 that have not been addressed by others.

* A core C language with a small step operational semantics. The
operational semantics is non-deterministic due to unspecified
expression evaluation order.

* An explicit type system for the core language that enjoys type
preservation and progress.

* A type sound translation of actual C programs into the core language.

* An executable semantics that has been proven sound and complete with
respect to the operational semantics.

* Extensions of separation logic to reason about subtle constructs in
C like non-determinism in expressions, and gotos in the presence of
block scope variables.

Name(s):Brigitta Hansen
Phone:0681 93039102
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Christian Klein, 10/13/2016 04:07 PM
  • Brigitta Hansen, 12/08/2015 02:46 PM -- Created document.