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.