Valérie Murat

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.

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

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 → q₁, b → q₂, g(q₁) → q₃, f(q₃,q₂) → q_f} 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