Bounded Model Checking and Feature Omission Diversity
This addresses a specific bottleneck in formal verification for software and hardware engineers, but it is incremental as it adapts an existing technique from software testing.
The paper tackles the problem of speeding up counterexample discovery in bounded model checking by using parallel runs with randomly disabled features, resulting in a decrease in average time to find counterexamples.
In this paper we introduce a novel way to speed up the discovery of counterexamples in bounded model checking, based on parallel runs over versions of a system in which features have been randomly disabled. As shown in previous work, adding constraints to a bounded model checking problem can reduce the size of the verification problem and dramatically decrease the time required to find counterexample. Adapting a technique developed in software testing to this problem provides a simple way to produce useful partial verification problems, with a resulting decrease in average time until a counterexample is produced. If no counterexample is found, partial verification results can also be useful in practice.