Ceta is a library for reasoning about combinations of equational tree languages. It supports emptiness testing of tree languages definable by a boolean combination of regular tree automaton over an equational theory containing operators that are associative and/or commutative with identity symbols. Ceta is based on propositional tree automata, and offers algorithms and datastructures for representing tree automata, combining tree automata using boolean operations, and testing emptiness.
Ceta is currently being used in the Maude Sufficient Completeness checker, and ACTAS a reachability analysis tool. Using Ceta, ACTAS has been able to verify the security of the Diffie-Hellman key-exchange protoco" and Shamir's three-path protocol without approximation techniques.
Ceta is being developed at the University of Illinois at Urbana-Champaign in the United States as part of a joint project with National Institute of Advanced Industrial Science and Technology in Japan. The primary software developer is Joe Hendrix with significant support from Josè Meseguer of UIUC and Hitoshi Ohsaki of AIST.
The project is currently in active development, and a number of key planned features have not yet been implemented. An alpha version is now available which supports combining equational tree automata and testing emptiness of automaton that are associative, commutative, and free. We do not yet support support rules with constraints, but that is planned for a future release. Ceta is available under the GPL license.
The source code for Ceta is now available as a gzipped tar file. Building Ceta requires the followig be installed:
The following files are available for download:
|ceta-alpha4.tar.gz||Source gzipped tar||2007-02-05|
|ceta-alpha3a.tar.gz||Source gzipped tar||2006-03-06|
|ceta-alpha2.tar.gz||Source gzipped tar||2005-11-17|
|ceta-alpha1.tar.gz||Source gzipped tar||2005-09-12|
Due to the alpha nature of Ceta and the current world of C++ ABI compatibilities, we do not offer a precompiled version of Ceta at this time.
Ceta's documentation is automatically generated using Doxygen. A copy of the documentation is included in the source, but may also be browsed online.
If you are interested in doing development on the library, please contact Joe Hendrix to discuss ideas for improving Ceta and how to add your code to the main repository.