Georg Stefan Schmid and Viktor Kunčak. Generalized arrays for Stainless frames. In Bernd Finkbeiner and Thomas Wies, editors, Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 332--354. Springer International Publishing, 2022.

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.

[ bib ] Back