Proving and Disproving Programs with Shared Mutable Data
share
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.
READ FULL TEXT