Communications of the ACM
Research Archive
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.