Communications of the ACM

Latest Research

From Communications of the ACM

Technical Perspective: The Scalability of CertiKOS

The authors of "Building Certified Concurrent OS Kernels" illustrate that formal verification can scale up to a moderate-size program (6,500 lines of C) that has... Andrew W. Appel
From Communications of the ACM | October 2019

From Communications of the ACM

Building Certified Concurrent OS Kernels

In this work, we present CertiKOS, a novel compositional framework for building verified concurrent OS kernels. Ronghui Gu, Zhong Shao, Hao Chen, Jieung Kim, Jérémie Koenig, Xiongnan (Newman) Wu, Vilhelm Sjöberg, David Costanzo
From Communications of the ACM | October 2019