Evidence-based model checking

Abstract

This paper shows that different “meta-model-checking” analyses can be conducted efficiently on a generic data structure we call a support set. Support sets may be viewed as abstract encodings of the “evidence” a model checker uses to justify the yes/no answers it computes. We indicate how model checkers may be modified to compute supports sets without compromising their time or space complexity. We also show how support sets may be used for a variety of different analyses of modelchecking results, including: the generation of diagnostic information for explaining negative model-checking results; and certifying the results of model checking (is the evidence internally consistent?).