Bug hunting with false negatives

Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs. Here we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from an abstract violation scenario. The violation pattern represents multiple violation scenarios, increasing the chance that a corresponding concrete violation exists. Then we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques.