Campus Event Calendar
Event Entry
What and Who
Formal Verification of Realistic Compilers
Zaynah Dargaye
ENSIIE, Evry
SWS Colloquium
SWS, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 13 May 2009
15:00
90 Minutes
E1 5
Wartburg, 5th floor
Saarbrücken
Abstract
It is generally expected that the compiler is semantically
transparent, that is, produces executable code that behaves as
prescribed by the semantics of the source code. However, compilers --
and especially optimizing compilers, which attempt to increase the
efficiency of generated code through program analyses and
transformations -- are highly complex software systems that perform
delicate symbolic computations. Bugs in the compiler are therefore
unavoidable : they can cause wrong code to be produced from a correct
source code
The CompCert project investigates the formal verification
of realistic compilers usable for critical embedded software. Such
verified compilers come with a mathematical, machine-checked proof
that the generated executable code behaves exactly as prescribed by
the semantics of the source program. By ruling out the possibility of
compiler-introduced bugs, verified compilers strengthen the guarantees
that can be obtained by applying formal methods to source programs.
This talk describes the formal verification of compilers and focuses
on two experimentation : the C CompCert compiler and the MLCompCert
compiler. MLCompCert is the mechanically verified compiler for the
purely functional fragment of ML that I have developed and verified
in Coq in my Ph. D. thesis.
transparent, that is, produces executable code that behaves as
prescribed by the semantics of the source code. However, compilers --
and especially optimizing compilers, which attempt to increase the
efficiency of generated code through program analyses and
transformations -- are highly complex software systems that perform
delicate symbolic computations. Bugs in the compiler are therefore
unavoidable : they can cause wrong code to be produced from a correct
source code
The CompCert project investigates the formal verification
of realistic compilers usable for critical embedded software. Such
verified compilers come with a mathematical, machine-checked proof
that the generated executable code behaves exactly as prescribed by
the semantics of the source program. By ruling out the possibility of
compiler-introduced bugs, verified compilers strengthen the guarantees
that can be obtained by applying formal methods to source programs.
This talk describes the formal verification of compilers and focuses
on two experimentation : the C CompCert compiler and the MLCompCert
compiler. MLCompCert is the mechanically verified compiler for the
purely functional fragment of ML that I have developed and verified
in Coq in my Ph. D. thesis.
Contact
Claudia Richter
688
--email hidden
Video Broadcast
Yes
Saarbrücken
E1 4
019
passcode not visible
logged in users only
Claudia Richter, 05/08/2009 10:34 -- Created document.