## 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).

## Tools

### TimbukLTA

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

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

## Teachings

### 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 OpenOffice.org Writer and OpenOffice.org Calc.
UE BUR (BUReautique) ‒ L1 Informatique ‒ Université de Rennes 1 ‒ 2012-2013

## Publications

### International Conferences and Workshops

[BDM11]
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
[GLLM13]
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

[GLLM12]
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