The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Refinement-Based Game Semantics for Certified Components

Last modified: Sat Oct 3 01:54:42 2020 GMT.

Author

Jérémie Koenig

Abstract

Current practices ensure software reliability through careful testing, but while testing can reveal the presence of bugs, it cannot entirely guarantee their absence. By contrast, certified systems come with a formal specification and a computer-checked proof of correctness, providing strong evidence that the system behaves as expected in all possible scenarios. Over the past decade, researchers have been able to build certified systems of significant size and complexity, including compilers, processor designs, operating system kernels and more.

Building on these successes, the DeepSpec project seeks to assemble them as certified components to build large-scale heterogeneous certified systems. However, by necessity, these certified components use a broad variety of semantic models and verification techniques. To connect them, we must first embed them into a common, general-purpose model. The work I present here proposes to combine game semantics, algebraic effects and the refinement calculus to build models suitable for this task. In particular, certified abstraction layers and the certified compiler CompCert can be embedded into a single framework supporting heterogeneous components, stepwise refinement, and data abstraction.

Published

Ph.D. Dissertation. Dept. of Computer Science, Yale University, September 2020.

Copyright © 1996-2021 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon