Last modified: Sat Oct 17 21:17:38 2020 GMT.
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.