关键词: 程序验证 程序测试 有穷自动机 有穷状态验证 有穷路径验证

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