Research Themes

Verification of infinite state systems

Computer systems are used everywhere, and we need to ensure that they are reliable. Formal verification of a system provides an accurate diagnosis for a given property and gives a counter-example if the property is unverified.
To verify some interesting systems like security protocols, networks or Java programs, we need to consider an infinite state space. ARTMC (Abstract Tree Regular Model Checking) allows to verify safety properties on infinite state systems using tree automata and tree transducers, or term rewriting systems.

Term Rewriting, Reachabilility Analysis, Safety Properties

Safety properties verify that there is no reachable state of the system which unsatisfy the property, i.e. no bad state. To verify a safety property, we have to compute the set of all possible reachable states, and verify that there is no bad state in this set, thanks to an intersection operation. We call this verification a reachability analysis.
When states are represented by terms, the set of reachable states is calculated thanks to a tree transducer or a term rewriting system. A term rewriting system is a set of rewrite rules l → r for rewriting set of terms.
For example, f(x,y) → f(g(x),g(y)) is a rewrite rule, and the term f(a,b) is rewrited this way: f(a,b) → f(g(a),g(b)) → f(g(g(a)),g(g(b))) → f(g(g(g(a))),g(g(g(b)))) → ...

Tree Automata

In ARTMC (Abstract Tree Regular Model Checking), a configuration (or a state) of the system is represented by a term, i.e. a word built with functional symbols which can be represented by a tree (ex: f(g(a),b) ).
A (possibly infinite) set of terms is represented by a tree automaton, composed by a set of states, a set of final states, an alphabet of functional symbols, and a set of normalized transitions. For example, the following set of transitions of a tree automaton {a → q1, b → q2, g(q1) → q3, f(q3,q2) → qf} can recognize the term f(g(a),b).



TimbukLTA is an extension of Timbuk, i.e., a tree automata completion engine for reachability analysis over Term Rewriting Systems. This extension uses Lattice Tree Automata to represent (efficiently) built-in values such as integers, strings, etc., and improves a lot the efficiency of verification of Java programs (see Publications → Technical Reports).
Source code and informations.
© 2012 ‒ Thomas Genet, Valérie Murat and Tristan Le Gall


CopsterLTA is an extension of Copster. From a .class file obtained from the compilation of .java files, Copster produces a Term Rewriting System (TRS) simulating the execution of the Java program. CopsterLTA uses built-in integer arithmetic instead of Peano arithmetic as in the original Copster. CopsterLTA also incorporates conditional rewriting rules.
Source code and informations.
© 2012 ‒ Valérie Murat, Nicolas Barré, Laurent Hubert, Luka Le Roux and Thomas Genet


Science popularization

  • Science popularization in Highschool classes: Cryptography and Security Protocols on the Internet ‒ 2010-2011.
    PDF of the presentation. (in french)

Courses and practical sessions

    Courses given in University of Rennes 1, more precisely at ISTIC.
  • Programming methods in UML.
    UE METH (Méthodes de programmation) ‒ L3 Informatique ‒ Université de Rennes 1 ‒ 2011-2012
    UE BMO (Bases de la Modélisation par Objets) ‒ L3 Informatique ‒ Université de Rennes 1 ‒ 2012-2013
  • Architecture of computer systems: programming in Scheme.
    UE ASI (Architecture des Systèmes Informatiques) ‒ L1 Informatique ‒ Université de Rennes 1 ‒ 2011-2013
  • Programming bases: programming in Java.
    UE FOR (Fonctionnement des ORdinateurs) ‒ L1 Informatique ‒ Université de Rennes 1 ‒ 2011-2012
  • Office: using Writer and Calc.
    UE BUR (BUReautique) ‒ L1 Informatique ‒ Université de Rennes 1 ‒ 2012-2013


International Conferences and Workshops

Y. Boichut, T.-B.-H. Dao and V. Murat. Characterizing Conclusive Approximations by Logical Formulae. Proceedings of 5th International Workshop on Reachability Problems, Lecture Notes in Computer Science, vol. 6945. 2011. PDF
T. Genet, T. Le Gall, A. Legay and V. Murat. A Completion Algorithm for Lattice Tree Automata. Proceedings of 18th International Conference on Implementation and Application of Automata (CIAA'13). To be published. 2013.

Technical Reports

T. Genet, T. Le Gall, A. Legay and V. Murat. Tree Regular Model Checking of Lattice-Based Automata. Technical Report RT-0424, INRIA. 2012. PDF