
handle: 11562/323061
Vacuum cleaning is a mandatory process when an implementation is verified with respect to a specification modeled by means of formal properties. In fact, vacuum cleaning looks for properties that, passing vacuously (e.g., an implication whose antecedent is always false), may lead verification engineers to a false sense of safety. Current approaches to vacuum cleaning, generally, exploit formal methods to provide an interesting witness proving that a property does not pass vacuously. However, such approaches are as complex as model checking, and they require to define and model check further properties, thus increasing the verification time. This paper proposes an alternative approach, based on fault simulation, that requires neither the definition of new properties, nor the use of model checking. Experimental results show the high efficiency of this approach.
vacuity analysis; Fault simulation
vacuity analysis; Fault simulation
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
