Autograph is now part of TRAG

Made with Lisp

What is Autograph

Autograph is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autograph is an experimental tool written in Common Lisp for verifying properties of graphs of bounded clique-width. It is written in Steele Bank Common Lisp ( SBCL). It uses the Autowrite library which provides the operations needed to create and manipulate automata. The following famous theorem connects the problem of verifying graph properties with term automata.

Monadic second-order model checking is for tree-width [Courcelle (1990)]
and clique-width [Courcelle, Makowski, Rotics (2001)].

Tree-width and clique-width are graph complexity measures based on graph decompositions. A decomposition produces a term representation of the graph. For a graph property expressed in monadic second order logic (MSO), the algorithm verifying the property takes the form of a term automaton which recognizes the terms denoting graphs satisfying the property.

Main features of Autograph

Obtaining Autograph

Autograph is now part if the TRAG project (Term Rewriting Automata and Graphs) available on BitBucket:
 git clone 

Contact information

Should you have any comments or suggestions regarding Autograph, or ideas on new functionalities that you would like to see in future releases of Autograph, please send them to


B. Courcelle. Graph Structure and Monadic Second-Order Logic. 2011
Cambridge University Press

B. Courcelle and I. Durand. Verifying monadic second order graph properties with tree automata. Proceedings of the 3rd European Lisp Symposium, pages 7-21, 2010
I. Durand. Implementing huge term automata. Submitted to the 4th European Lisp Symposium, 2011.

Pointers to relevant sites

Here are some pointers to other sites with similar interests, listed by topic.

Sites and people

Steele Bank Common Lisp (SBCL)
Irčne Durand
Bruno Courcelle