Inherent vacuity for GR(1) specifications

Abstract

Vacuity is a well-known quality issue in formal specifications, studied mostly in the context of model checking. Inherent vacuity is a type of vacuity that applies to specifications, without the context of a model. GR(1) is an expressive assume-guarantee fragment of LTL, which enables efficient symbolic synthesis.

BibTeX

@inproceedings{Maoz-Shalom:FSE20,
  author    = {Shahar Maoz and
               Rafi Shalom},
  title     = {Inherent vacuity for {GR(1)} specifications},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {99--110},
  publisher = {{ACM}},
  year      = {2020},
}

Inherent vacuity for GR(1) specifications

Abstract

Related papers