# Efficient Generation of Inductive Validity Cores for Safety Properties

## E. Ghassabani, A. Gacek, M. Whalen

### Foundations of Software Engineering, November 2016

Symbolic model checkers can construct proofs of properties over very
complex models. However, the results reported by the tool when a proof
succeeds do not generally provide much insight to the user. It is
often useful for users to have traceability information related to the
proof: which portions of the model were necessary to construct it.
This traceability information can be used to diagnose a variety of
modeling problems such as overconstrained axioms and underconstrained
properties, and can also be used to measure completeness of a set of
requirements over a model. In this paper, we present a new algorithm
to efficiently compute the inductive validity core (IVC) within a
model necessary for inductive proofs of safety properties for
sequential systems. The algorithm is based on the UNSAT core support
built into current SMT solvers and a novel encoding of the inductive
problem to try to generate a minimal inductive validity core. We prove
our algorithm is correct, and describe its implementation in the JKind
model checker for Lustre models. We then present an experiment in
which we benchmark the algorithm in terms of speed, diversity of
produced cores, and minimality, with promising results.