TACE

TACE is an OCaml library implementing procedures for the construction and decision of several classes of Tree Automata with Constraints of Equality modulo Equational Theories.

It designed as a specialized first order theorem prover, following the approach presented in Tree automata with equality constraints modulo equational theories, JLAP 75(2) 2008 - coauthored with Michaël Rusinowitch, and Laurent Vigneron.

The library TACE has been applied to the verification of security protocols in models with explicit destructors. It was also used as an algorithmic toolbox for the integration of decision procedures in inductive theorem proving procedures and later for the problems of XML static typechecking the verification of XML access control policies.