I contrast the paradigm of SMT-based verification of software, such as in LiquidHaskell with the approach based on automata. To me it appears that automata are only used in the paradigm of model checking.
It also seems to me this paradigm has severe difficulties to scale to the verification of programs. In fact, I recall hearing Joseph Sifakis quoting a member of his PhD jury saying "there are no finite state programs out there".
Of course, there are (like protocols), but does automata scale to the full verification of software as well as the SMT-based + specification approach?