Verification in Isabelle/HOL of Hopcroft's algorithm for minimizing DFAs including runtime analysis

Research project supervised by Tobias Nipkow, based on previous work of Peter Lammich and Thomas Türk. This project is also my final year intership as a student at the French engineering school École Nationale Supérieure des Mines de Nancy, University of Lorraine.

The main theory is in Hopcroft_Minimisation.thy.

A bimonthly progress report can be found in Progress_Report.

A $\LaTeX$ report can be found in proof.tex. It contains the paper proof for time complexity.