Autowrite is a project carried out at the Laboratoire Bordelais de Recherche en Informatique (LaBRI) of the Université Bordeaux I, by the LLA (Logic, Formal Languages and Applications) team. Autowrite is an experimental tool written in CMU Common Lisp for checking properties of term rewrite systems. It was initially designed to check call-by-need (CBN) properties of TRSs. For this purpose, it implements the tree automata constructions used in the decidability proofs of the call-by-need properties and many useful operations on terms, TRSs and tree automata. This new version of Autowrite includes new functionalities related to TRSs, timing information but the most interesting new feature is the possibility to handle directly (load, save, combine) bottom-up tree automata. The graphical interface (still under construction) running under X11 is written using FreeCLIM , the free implementation of the CLIM specification . From this interface, one can handle TRSs, tree automata and build many tree automata related to TRSs. one can check membership to CBN for the different approximations of a given system.
The principal features of Autowrite are:
The Autowrite distribution is publically available for research purposes.
The Autowrite distribution consists of a Linux gzip-compressed tar file.
The currently supported machines and operating systems are listed below.
A collection of examples of term rewrite systems to use with Autowrite is included in the Data directory of the distribution.
Download the relevant Autowrite.tgz tar file
Please refer to the Autowrite user's guide to see how to use Autowrite. Also available in Postscript or PDF
Should you have any comments or suggestions regarding Autowrite, or ideas on new functionalities that you would like to see in future releases of Autowrite, please send them to idurand@labri.fr.
Other Releases
F. Jacquemard. Decidable approximations of term rewriting systems.
In Proc. 7th RTA, volume 1103 of LNCS, pages 362--376, 1996.
H. Comon. Sequentiality, Monadic Second Order Logic and Tree Automata.
Information and Computation, 157:25--51, 2000.
I.Durand and A.Middeldorp. On the complexity of deciding call-by-need.
Technical Report 1194-98, LaBRI, Université de Bordeaux I, 1998.
I.Durand and A.Middeldorp. On the modularity of deciding call-by-need.
In Proc. FoSSaCS'01, volume 2030 of LNCS, pages 199-213, 2001
H. Comon and M. Dauchet and R. Gilleron and F. Jacquemard and D. Lugiez a
nd S. Tison and M. Tommasi.
Tree Automata Techniques and Applications.
Here are some pointers to other sites with similar interests, listed by topic.