Modern clouds depend crucially on an extensible ecosystem of thousands of controllers,
each managing critical systems (eg, a ZooKeeper cluster). A controller continuously …

This paper reports our experience applying lightweight formal methods to validate the
correctness of ShardStore, a new key-value storage node implementation for the Amazon …

We introduce an unusual approach for implementing cryptographic arithmetic in short high-
level code with machinechecked proofs of functional correctness. We further demonstrate …

This paper presents Serval, a framework for develo** automated verifiers for systems
software. Serval provides an extensible infrastructure for creating verifiers by lifting …

File systems are too large to be bug free. Although handwritten test suites have been widely
used to stress file systems, they can hardly keep up with the rapid increase in file system …

This paper describes an approach to designing, implementing, and formally verifying the
functional correctness of an OS kernel, named Hyperkernel, with a high degree of proof …

We present a new approach to testing file-system crash consistency: bounded black-box
crash testing (B3). B3 tests the file system in a black-box manner using workloads of file …

The promise of software sandboxing is flexible, fast and portable isolation; capturing the
benefits of hardwarebased memory protection without requiring operating system …

This paper introduces Perennial, a framework for verifying concurrent, crash-safe systems.
Perennial extends the Iris concurrency framework with three techniques to enable crash …

Recent non-volatile memory technologies such as 3D XPoint and NVDIMMs have enabled
persistent memory (PM) systems that can manipulate persistent data directly in memory. This …