The h1 Tool SuiteJean Goubault-Larrecq |
LSV/UMR 8643, CNRS, ENS Cachan & INRIA Futurs projet SECSI |
61 avenue du président-Wilson, F-94235 Cachan Cedex |
goubault@lsv.ens-cachan.fr |
Phone: +33-1 47 40 75 68 Fax: +33-1 47 40 75 21 |
Abstract: This describes the theoretical basis and practical usage of the h1 tool suite. This is a set of tools that allow one to handle tree-regular languages in various formats, including deterministic, non-deterministic, and alternating finite tree automata, but also various fairly general clausal formats, the central one being the H_{1} class due to Nielson, Nielson, and Seidl. Alternatively, this can also be seen as a terminating automated theorem prover for the H_{1} class; or as an automated theorem prover for general clause sets, which however makes some controlled mistakes in the spirit of abstract interpretation: this is notably useful in proofs of security protocols. Other aspects of the h1 tool suite include producing certain forms of automated proofs by induction in the Coq proof assistant, deciding Presburger arithmetic, and displaying tree automata.
This document was translated from L^{A}T_{E}X by H^{E}V^{E}A.