A number of tools have been developed for carrying out separation-logic proofs
mechanically using an interactive proof assistant. One of the most advanced such tools is …

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

Modern programming languages, ranging from Haskell and ML, to JavaScript, C# and Java,
all make extensive use of higher-order state. This paper advocates a new verification …

Many algorithms can be implemented most efficiently with imperative data structures. This
paper presents Sepref, a stepwise refinement based tool chain for the verification of …

Step-indexed separation logic has proven to be a powerful tool for modular reasoning about
higher-order stateful programs. However, it has only been used to reason about safety …

Dijkstra monads enable a dependent type theory to be enhanced with support for specifying
and verifying effectful code via weakest preconditions. Together with their closely related …

This paper presents a framework aimed at significantly reducing the cost of proving
functional correctness for low-level operating systems components. The framework is …

The higher-order logic found in proof assistants such as Coq and various HOL systems
provides a convenient setting for the development and verification of functional programs …

Steel is a language for developing and proving concurrent programs embedded in F⋆, a
dependently typed programming language and proof assistant. Based on SteelCore, a …

Tezos is a blockchain launched in June 2018. It is written in OCaml and supports smart
contracts. Its smart contract language is called Michelson and it has been designed with …