A beginner guide to Iris, Coq and separation logic

TL;DR

This paper is a comprehensive beginner's guide to using Iris, Coq, and separation logic for formal verification of concurrent algorithms, emphasizing detailed explanations, tactics, and foundational concepts.

Contribution

It offers an in-depth, accessible introduction to Iris and separation logic, including practical examples and tactics, tailored for newcomers in formal verification.

Findings

Enhanced understanding of Iris and separation logic for beginners

Detailed walkthroughs of verification examples and tactics

Resources and references for further learning

Abstract

Creating safe concurrent algorithms is challenging and error-prone. For this reason, a formal verification framework is necessary especially when those concurrent algorithms are used in safety-critical systems. The goal of this guide is to provide resources for beginners to get started in their journey of formal verification using the powerful tool Iris. The difference between this guide and many others is that it provides (i) an in-depth explanation of examples and tactics, (ii) an explicit discussion of separation logic, and (iii) a thorough coverage of Iris and Coq. References to other guides and to papers are included throughout to provide readers with resources through which to continue their learning.