Abstract: Finite state verification for programs is an approach between theorem proving and testing. On the one hand, it can prove that a program has some required properties, or find counterexamples to prove the program does not have these properties. On the other

Key words: Software verification, Software testing, Finite automaton, Finite state verification, Finite path verification