This code package consists of 3 parts: 1) Certifying Fast Downward, an extension to Fast Downward which allows generation of proofs for A* with hmax, hm and M&S heuristics. 2) Certifying fd-hc-refinement, an extension to the fd-hc-refinement algorithm by Marcel Steinmetz which allows generation of proofs for the uc heuristic. 3) A standalone verifier which is able to verify proofs.

{"references": ["Salom\u00e9 Eriksson, Gabriele R\u00f6ger and Malte Helmert. A Proof System for Unsolvable Planning Tasks. In Proceedings of the 28th International Conference on Automated Planning and Scheduling (ICAPS). 2018."]}