Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
The C standard formalized in Coq
Robbert Krebbers
Aarhus University
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 15 December 2015
10:30
60 Minutes
E1 5
029
Saarbrücken
Abstract
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.
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.
Contact
Brigitta Hansen
0681 93039102
--email hidden
passcode not visible
logged in users only
Christian Klein, 10/13/2016 16:07
Brigitta Hansen, 12/08/2015 14:46 -- Created document.
Brigitta Hansen, 12/08/2015 14:46 -- Created document.