Campus Event Calendar
Event Entry
What and Who
Compositional Inter-Language Reasoning
Georg Neis
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
SWS, RG1
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 15 May 2013
15:00
60 Minutes
E1 5
005
Saarbrücken
Abstract
The correctness of a compiler is naturally phrased as a problem of program equivalence: any source program should be equivalent to the
result of compiling it. We want this notion of equivalence to be compositional such that (1) we can verify a compiler in a modular
fashion, and (2) we can link modules separately compiled by one or several verified compilers without losing the correctness guarantee.
Unfortunately, existing methods do not support both. With the help of "parametric bisimulations", which we introduced last year, we hope to
change this.
result of compiling it. We want this notion of equivalence to be compositional such that (1) we can verify a compiler in a modular
fashion, and (2) we can link modules separately compiled by one or several verified compilers without losing the correctness guarantee.
Unfortunately, existing methods do not support both. With the help of "parametric bisimulations", which we introduced last year, we hope to
change this.
Contact
Claudia Richter
9303 9103
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
112
passcode not visible
logged in users only
Claudia Richter, 05/16/2013 16:38 -- Created document.