Abstract This paper presents , a new intermediate verification language and deductive verification tool that provides inbuilt support for concurrency reasoning. ’s meta-theory is based on the higher-order concurrent separation logic Iris, incorporating core features such as user-definable ghost state and thread-modular reasoning via shared-state invariants. To achieve better accessibility and enable proof automation via SMT solvers, restricts Iris to its first-order fragment. The entailed loss of expressivity is mitigated by a higher-order module system that enables proof modularization and reuse. We provide an overview of the language and describe key aspects of the supported proof automation. We evaluate on a benchmark suite of verification tasks comprising linearizability and memory safety proofs for common concurrent data structures and clients as well as one larger case study. Our evaluation shows that improves over existing proof automation tools for Iris in terms of verification times and usability. Moreover, the tool significantly reduces the proof overhead compared to proofs constructed using the Iris/Rocq proof mode.

Abstract Memory safety is a fundamental correctness property of software. For programs that manipulate linked, heap-allocated data structures, ensuring memory safety requires analyzing their possible shapes. Despite significant advances in shape analysis, existing techniques rely on hand-crafted domains tailored to specific data structures, making them difficult to generalize and extend. This paper presents a novel approach that reduces memory-safety proofs to the verification of heap-less imperative programs, enabling the use of off-the-shelf software verification tools. We achieve this reduction through two complementary program instrumentation techniques: space invariants, which enable symbolic reasoning about unbounded heaps, and flow abstraction, which encodes global heap properties as local flow equations. The approach effectively verifies memory safety across a broad range of programs, including concurrent lists and trees that lie beyond the reach of existing shape analysis tools.

We introduce the well structured problem as the question of whether a model (here a counter machine) is well structured (here for the usual ordering on integers). We show that it is undecidable for most of the (Presburger-defined) counter machines except for Affine VASS of dimension one. However, the strong well structured problem is decidable for all Presburger counter machines. While Affine VASS of dimension one are not, in general, well structured, we give an algorithm that computes the set of predecessors of a configuration; as a consequence this allows to decide the well structured problem for 1-Affine VASS.