The Verification of Conversion Algorithms between Finite Automata

ABSTRACT. This paper presents three verified conversion algorithms between finite automata in Isabelle/HOL. The specifications of all algorithms are formalized in a direct way, from which Isabelle/HOL can generate executable programs. The correctness of each algorithm is totally verified from three perspectives: the loops in each algorithm terminate, the output of an algorithm is an automata with the expected type, and the input and output of one conversion algorithm accept the same language. The whole work includes over 3000 lines of code in Isabelle/HOL.