Verifying the Option Type with Rely-Guarantee Reasoning

Abstract

Many programming languages include an implementation of the option type, which encodes the absence or presence of values. Incorrect use of the option type results in run-time errors, and unstylistic use results in unnecessary code. Researchers and practitioners have tried to mitigate the pitfalls of the option type, but have yet to evaluate tools for enforcing correctness and good style.

BibTeX

@inproceedings{Yoo-al:ASE24,
  author    = {James Yoo and
               Michael D. Ernst and
               Ren{\'{e}} Just},
  title     = {Verifying the Option Type with {Rely-Guarantee} Reasoning},
  booktitle = {ASE},
  pages     = {367--380},
  publisher = {{ACM}},
  year      = {2024},
}

Verifying the Option Type with Rely-Guarantee Reasoning

Abstract

Related papers