Abstract Development of formal proofs of correctness of programs can increase actual and
perceived reliability and facilitate better understanding of program specifications and their …

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

The main contribution of this paper is GoJournal, a verified, concurrent journaling system
that provides atomicity for storage applications, together with Perennial 2.0, a framework for …

Verifying the DaisyNFS concurrent and crash- safe file system with sequential reasoning
Page 1 This paper is included in the Proceedings of the 16th USENIX Symposium on …

The days of verifying only toy programs are long gone. The last two decades have marked a
new era of verification at scale, bringing strong guarantees to large and critical systems—an …

Guarded Kleene Algebra with Tests (GKAT) is a fragment of Kleene Algebra with Tests
(KAT) that was recently introduced to reason efficiently about imperative programs. In …

Distributed systems are hard to design and implement correctly. Recent work has tried to
use formal verification techniques to provide rigorous correctness guarantees. These works …

Crash-safety is an important property of real systems, as the main functionality of some
systems is resilience to crashes. Toward a compositional verification approach for crash …

Critical systems software such as the file system is challenging to make correct due to the
combination of concurrency in the implementation for good performance and the …

In 1984, Robin Milner proposed a nonstandard interpretation of regular expressions: as
behaviours of nondeterministic processes rather than regular languages. This shift in …