EHMTT Verifier

This page provides a web interface to a program verification tool which can check whether a given tree-processing functional program satisfies a given specification expressed by using a top-down deterministic tree automaton. The following papers explain how the verification tool works internally:
Verification of Tree-Processing Programs via Higher-Order Model Checking
Hiroshi Unno, Naoshi Tabuchi, and Naoki Kobayashi
In the Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS 2010), Springer, Lecture Notes in Computer Science 6461, pp.312-327, Shanghai, China, November/December, 2010.
[short version PDF] [full version PDF]

Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification
Naoki Kobayashi, Naoshi Tabuchi, and Hiroshi Unno
In the Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), pp.495-508, Madrid, Spain, January, 2010.
[short version PDF] [full version PDF]

Enter a program and its specification in the box below, and press the "verify" button.