MC/DC coverage prescribes a set of \emph{MC/DC sequences}.
Such a sequence is defined by a specification of the
truth values of certain atomic boolean expressions which appear in
predicates (i.e. boolean combinations of atomic boolean expressions) in
the program. An execution trace \emph{satisfies} the sequence if it
\emph{realizes} the atomic boolean conditions in accordance with the truth
value specification of the sequence. An MC/DC sequence is \emph{feasible}
if there is one such execution trace. The overall goal for an MC/DC test
generator is, for each sequence: if \emph{feasible}, to
generate a test input realizing the sequence; otherwise,
to \emph{prove} that the sequence is infeasible.

In this paper, we propose a method whose aim is \emph{optimal} MC/DC
coverage for bounded programs, i.e. for each MC/DC sequence, the
method either produces a test input, or proves that sequence is
infeasible. The method is based on symbolic execution with
interpolation, and in this paper, we present a \emph{customized}
interpolation algorithm. We then present a comprehensive experimental
evaluation comparing with the only available system CBMC
which can operate on reasonably large programs, and further, which can
provide optimal coverage for many examples. We will use a benchmark based
on RERS which contains the kinds of reactive programs for which MC/DC
was motivated by. We show that our method, by a significant margin,
surpasses CBMC. In particular, our method often produces an
\emph{optimal} MC/DC result.