Generalized Arrays for Stainless Frames

paper ps   
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.

Citation

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.

BibTex Entry

@inproceedings{SchmidKuncak22StainlessFrames,
  author = {Schmid, Georg Stefan
 and Kun{\v{c}}ak, Viktor},
  editor = {Finkbeiner, Bernd
and Wies, Thomas},
  title = {Generalized Arrays for {S}tainless Frames},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = {2022},
  publisher = {Springer International Publishing},
  pages = {332--354},
  abstract = {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.},
  isbn = {978-3-030-94583-1}
}