Campus Event Calendar
Event Entry
What and Who
Correctness of a Compiler for (Just Slightly) Restricted C
Dirk Leinenbach
Ringvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 11 November 2004
13:00
-- Not specified --
45
016
Saarbrücken
Abstract
In the Verisoft project of the German federal government we use the
C-like programming language C0 for the implementation of most programs
including large parts of an operating system micro kernel. Another
part of the project is the formal verification of a simple non
optimizing compiler for C0.
We will start this talk with a short introduction of the language C0.
Afterwards we will explain the overall structure of the C0 compiler
(which is partitioned into a functional part and a part which is
written in C0 itself) and then present a proof sketch for the formal
verification of the compiler.
C-like programming language C0 for the implementation of most programs
including large parts of an operating system micro kernel. Another
part of the project is the formal verification of a simple non
optimizing compiler for C0.
We will start this talk with a short introduction of the language C0.
Afterwards we will explain the overall structure of the C0 compiler
(which is partitioned into a functional part and a part which is
written in C0 itself) and then present a proof sketch for the formal
verification of the compiler.
Contact
--email hidden
passcode not visible
logged in users only
Bahareh Kadkhodazadeh, 11/08/2004 10:46
Bahareh Kadkhodazadeh, 10/14/2004 12:04 -- Created document.
Bahareh Kadkhodazadeh, 10/14/2004 12:04 -- Created document.