Iris is a framework for higher-order concurrent separation logic, which has been implemented
in the Coq proof assistant and deployed very effectively in a wide variety of verification …

Rust is a new systems programming language that promises to overcome the seemingly
fundamental tradeoff between high-level safety guarantees and low-level control over resource …

When using a proof assistant to reason in an embedded logic -- like separation logic -- one
cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in …

Concurrent separation logics (CSLs) have come of age, and with age they have accumulated
a great deal of complexity. Previous work on the Iris logic attempted to reduce the complex …

The development of concurrent separation logic (CSL) has sparked a long line of work on
modular verification of sophisticated concurrent programs. Two of the most important features …

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 the Iris Proof …

The C programming language was created by Thompson and Ritchie around 1970 as the
implementation language of the Unix operating system [Rit93]. The development of Unix …

Rust is a modern systems programming language whose ownership-based type system
statically guarantees memory safety, making it particularly well-suited to the domain of safety-…

Given the central role that C continues to play in systems software, and the difficulty of writing
safe and correct C code, it remains a grand challenge to develop effective formal methods …

… BY RALF JUNG, JACQUES-HENRI JOURDAN, ROBBERT KREBBERS, AND DEREK
DREYER … Krebbers, R., Timany, A. and Birkedal, L. Interactive proofs in higher- order …