Vacuity Analysis for Property Qualification by Mutation of Checkers

The paper tackles the problem of property qualification focusing in particular on the identification of vacuous properties. It proposes a methodology based on a combination of dynamic and static techniques that, given a set of properties defined to check the correctness of a design implementation, performs vacuity detection. Existing approaches for vacuity checking are as complex as model checking, and they require to define and model check further properties, thus increasing the verification time. Moreover, for some formulae they fail to detect vacuity, as for example in case of tautology. These problems are overcome by our approach. It is based on mutation analysis, thus, it does not require the definition of new properties granting a speed-up of the vacuity analysis process. Moreover, it provides highly accurate vacuity alerts which capture also propositional and temporal tautologies.