AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Expert Audience

English

60 Minutes

Saarbrücken

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.

Brigitta Hansen

0681 93039102

--email hidden

Yes

Kaiserslautern

G26

113

passcode not visible

logged in users only