Proof that $A_{DFA}$ is decidable in Sipser
The computation will always halt. If $M$ doesn't reject right away, then $B$ is an encoding of a DFA. DFA always halt on any finite input, so the simulation must halt too.