This is an unofficial reimagining of the Archive of Formal Proofs
Formalizing Statecharts using Hierarchical Automataby Steffen Helke and Florian Kammüller