Proving and Disproving Programs with Shared Mutable Data

TL;DR

This paper introduces a verification tool for deterministic programs with shared mutable references, using a novel SMT-based encoding that improves automation and efficiency in proving safety and termination.

Contribution

The paper presents a new quantifier-free translation of programs with mutable references into purely functional forms, enabling effective use of SMT solvers for verification.

Findings

Effective verification of programs with shared mutable data.

Ability to report counterexamples and prove safety.

Maintains efficiency for purely functional data structures.

Abstract

We present a tool for verification of deterministic programs with shared mutable references against specifications such as assertions, preconditions, postconditions, and read/write effects. We implement our tool by encoding programs with mutable references into annotated purely functional recursive programs. We then rely on function unfolding and the SMT solver Z3 to prove or disprove safety and to establish program termination. Our tool uses a new translation of programs where frame conditions are encoded using quantifier-free formulas in first-order logic (instead of relying on quantifiers or separation logic). This quantifier-free encoding enables SMT solvers to prove safety or report counterexamples relative to the semantics of procedure specifications. Our encoding is possible thanks to the expressive power of the extended array theory of the Z3 SMT solver. In addition to the ability to report counterexamples, our tool retains efficiency of reasoning about purely functional layers of data structures, providing expressiveness for mutable data but also a significant level of automation for purely functional aspects of software. We illustrate our tool through examples manipulating mutable linked structures and arrays.