There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification “every request is eventually followed by an acknowledgment” is satisfied vacuously by a system that never generates any requests. Vacuous satisfaction misleads users of model-checking into thinking that a system is correct. It is a serious problem in practice. There are several existing definitions of vacuity. Originally, Beer et al.  formalized vacuity as insensitivity to syntactic perturbation (syntactic vacuity). This formulation captures the intuition of “vacuity” when applied to a single occurrence of a subformula. Armoni et al.
|There are no publications to display.|
Suggest a relevant paper: