The Research archive provides access to all Research articles published in past issues of Communications of the ACM.
October 2019
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 substantial shared-memory concurrency.
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.