Proving finite state machines correct with an automaton-based method