Efficient and Verified Computation of Simulation Preorders on NFAs

by Manuel Eberl

Bachelor's thesis at the Technical University of Munich (2012)


In this thesis, the algorithm presented by Ilie, Navarro, and Yu for computing simulation relations on Nondeterministic Finite Automata is implemented and verified with the interactive theorem prover Isabelle using Peter Lammich's Monadic Refinement Framework. This is done by writing an abstract version of the algorithm and proving it correct and then successively replacing parts of it with more concrete commands, proving the correctness of each modification, until an executable algorithm is obtained. This code can then be exported to programming languages such as ML, OCaml, Haskell or Scala.

Download PDF (467 KiB)


 author = {Eberl, Manuel},
 title = {Efficient and Verified Computation of Simulation Preorders on NFAs},
 year = {2012},
 month = {10},
 school = {Technical University of Munich},
 type = {Bachelor's thesis},
 note = {\url{https://www21.in.tum.de/~eberlm/pdfs/nfasim.pdf}}

Download BibTeX (300 Bytes)