Abstract The Verified Software Toolchain builds foundational machine-checked proofs of the
functional correctness of C programs. Its program logic, Verifiable C, is a shallowly …

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 CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for
a functional programming language to date. The architecture of the compiler, a sequence of …

We present VeriPhy, a verified pipeline which automatically transforms verified high-level
models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic (dL) to …

Modern SAT solvers can emit independently-checkable proof certificates to validate their
results. The state-of-the-art proof system that allows for compact proof certificates is …

Modern subgraph-finding algorithm implementations consist of thousands of lines of highly
optimized code, and this complexity raises questions about their trustworthiness. Recently …

Modern SAT solvers can emit independently checkable proof certificates to validate their
results. The state-of-the-art proof system that allows for compact proof certificates is …

Union-Find is a famous example of a simple data structure whose amortized asymptotic time
complexity analysis is nontrivial. We present a Coq formalization of this analysis, following …

Developing technology for building verified stacks, ie, computer systems with
comprehensive proofs of correctness, is one way the science of programming languages …

Program verification in the large is not only a matter of mechanizing a program logic to
handle the semantics of your programming language. You must reason in the mathematics …