  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.
