Formal Verification of Hierholzer s Algortithm