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
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)))) → ...
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
Source code and informations.
© 2012 ‒ Thomas Genet, Valérie Murat and Tristan Le Gall
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
Source code and informations.
© 2012 ‒ Valérie Murat, Nicolas Barré, Laurent Hubert, Luka Le Roux and Thomas Genet
.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