Viktor Kuncak, Georg Stefan Schmid
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 nov ...
Springer, Cham2022