Induction-Guided Falsification

Abstract. The induction-guided falsification searches a bounded reach-able state space of a transition system for a counterexample that the system satisfies an invariant property. If no counterexamples are found, it tries to verify that the system satisfies the property by mathematical induction on the structure of the reachable state space of the system, from which some other invariant properties may be obtained as lemmas. The verification and falsification process is repeated for each of the prop-erties until a counterexample is found or the verification is completed. The NSPK authentication protocol is used as an example to demonstrate the induction-guided falsification