CHOCKLER, KROENING, PURANDARE: COMPUTING MUTATION COVERAGE IN INTERPOLATION-BASED MODEL CHECKING 1 Computing Mutation Coverage in Interpolation-based Model Checking

Abstract—Coverage is a means to quantify the quality of a system specification, and is frequently applied to assess progress in system validation. Coverage is a standard measure in testing, but is very difficult to compute in the context of formal verifica-tion. We present efficient algorithms for identifying those parts of the system that are covered by a given property. Our algorithm is integrated into state-of-the-art SAT-based Model Checking using Craig interpolation. The key insight of our algorithm is the re-use of previously computed inductive invariants and counterexamples. This re-use permits a a rapid completion of the vast majority of tests, and enables the computation of a coverage measure with 96 % accuracy with only 5x the runtime of the Model Checker. Index Terms—Model Checking, Coverage, Interpolatio