1.
Philos Trans A Math Phys Eng Sci
; 375(2104)2017 Oct 13.
Artigo
em Inglês
| MEDLINE
| ID: mdl-28871053
RESUMO
We present recent work on building and scaling trustworthy systems with formal, machine-checkable proof from the ground up, including the operating system kernel, at the level of binary machine code. We first give a brief overview of the seL4 microkernel verification and how it can be used to build verified systems. We then show two complementary techniques for scaling these methods to larger systems: proof engineering, to estimate verification effort; and code/proof co-generation, for scalable development of provably trustworthy applications.This article is part of the themed issue 'Verified trustworthy software systems'.