We present a case study applying the k-induction method to
  equivalence checking of Simulink designs.  In particular, we are
  interested in the problem of equivalence detection in mutation-based
  testing: given a design S, determining whether a ``mutant'' design
  S' derived from S by syntactic fault injection is behaviourally
  equivalent to S. In this situation, efficient equivalence checking
  techniques are needed to avoid redundant and expensive search for
  test cases that observe differences between S and S'.  We have
  integrated k-induction into our test case generation framework for
  Simulink.  We show, using a selection of benchmarks, that
  k-induction can be effective in detecting equivalent mutants,
  sometimes as a stand-alone technique, and sometimes with some manual
  assistance.  We further discuss how the level of automation of the
  method can be increased by using static analysis to derive
  strengthening invariants from the structure of the Simulink models.