We present an approach for verification of programs with shared mutable references against specifications such as assertions, preconditions, postconditions, and read/write effects. We implement our tool in the Stainless verification system for Scala.

A novelty of our approach is a translation of imperative function contracts that encodes frame conditions using quantifier-free formulas in first-order logic, instead of relying on quantifiers or on dedicated separation logic reasoning. Our quantifier-free encoding enables SMT solvers to both prove safety and to report counterexamples relative to the semantics of procedure contracts. Our encoding is possible thanks to the expressive power of the extended array theory of de Moura and Bjørner, implemented in the SMT solver Z3, whose map operators allow us to project heaps before and after the call onto the declared reads and modifies clauses.

To support inductive proofs about the preservation of invariants, our approach permits capturing a projection of heap state as a history variable and evaluating imperative ghost code in the specified captured heap. This feature also allows us to explicitly state and prove hyperproperties such as independence on certain heap regions.

Another feature of our model is that we retain the efficiency of reasoning about purely functional layers of data structures, which need not be represented using heap references but often map directly to SMT-LIB algebraic data types and arrays. We thus obtain a combination of expressiveness for shared mutable data where needed, while retaining automation for purely functional program aspects. We illustrate our approach by proving detailed correctness properties of examples manipulating mutable linked structures.