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

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

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Trustworthy File Systems
Speaker:Christine Rizkallah
coming from:NICTA
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
Language:English
Date, Time and Location
Date:Monday, 21 September 2015
Time:13:00
Duration:60 Minutes
Location:Saarbr├╝cken
Building:E1 5
Room:029
Abstract

In this talk, I will present an approach to ease the verification of file-system
code using a domain-specific language, currently called CoGent, supported by
a self-certifying compiler that produces C code, a high-level specification, and
translation correctness proofs.

CoGent is a restricted, polymorphic, higher-order, and purely functional
language with linear types and without the need for a trusted runtime or
garbage collector. It compiles to efficient C code that is designed to
interoperate with existing C functions.

For a well-typed CoGent program, the compiler produces C code, a
high-level shallow embedding of its semantics in Isabelle/HOL, and a
proof that the C code correctly implements this embedding. The aim is
for proof engineers to reason about the full semantics of real-world
systems code productively and equationally, while retaining the
interoperability and leanness of C.

I will give a high-level overview of the formal verification stages of the
compiler, which include automated formal refinement calculi, a switch
from imperative update semantics to functional value semantics formally
justified by the linear type system, and a number of standard compiler phases
such as type checking and monomorphisation. The compiler certificate is a
series of language-level meta proofs and per-program translation validation
phases, combined into one coherent top-level theorem in Isabelle/HOL.
Contact
Name(s):Brigitta Hansen
Phone:0681 93039102
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:113
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
Created by:Brigitta Hansen/MPI-SWS, 09/18/2015 03:27 PMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:14 PM
  • Brigitta Hansen, 09/18/2015 03:29 PM -- Created document.