Summary
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.
News
- Feb. 4, 2007
- Released Alpha 4. This release should significantly improve the performance of the emptiness test with AC symbols, and adds support for membership.
Download
The source code for Ceta is now available as a gzipped tar file. Building Ceta requires the followig be installed:
- A C++ compiler (gcc 3.3 or later recommended)
- The Boost C++ Libraries (version 1.32 or later recommended)
- Doxygen (version 1.4 or later recommended).
The following files are available for download:
| Name | Format | Date |
| 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.
Documentation
Ceta's documentation is automatically generated using Doxygen. A copy of the documentation is included in the source, but may also be browsed online.
Announcement Mailing list
In order to be informed of new releases, users are strongly encouraged to subscribe to the ceta-announce mailing list. This is an announce only list used to notify subscribed about news related to Ceta's development. The traffic will be at most a few messages per month. Subscribe or unsubscribe at the ceta-announce homepage.Development
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.