Proving and Disproving Programs with Shared Mutable Data

Georg Schmid, Viktor Kunčak

We present a tool for verification of deterministic programs with shared mutable references against specifications such as assertions, preconditions, postconditions, and read/write…