Sign In

Communications of the ACM

Research Archive


Archives

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

Building Certified Concurrent OS Kernels

In this work, we present CertiKOS, a novel compositional framework for building verified concurrent OS kernels.