Treffer: Tree automata extensions for verification of infinite states systems ; Extensions des automates d'arbres pour la vérification de systèmes à états infinis

Computer systems are more and more important in everyday life, and errors into those systems can make dramatic damages. There are formal methods which can assure reliability of a system. The formal method used in this thesis is called tree automata completion and allows to analyze infinite state systems. In this representation, states of a system are represented by a term and sets of states by tree automata. The set of all reachable behaviors (or states) of the system is computed thanks to successive applications of a term rewriting system which represents the behavior of the system. The reliability of the system is assured by checking that no forbidden state is reachable by the system. But the set of reachable states is not always computable and we need to compute an over-approximation of it. This over-approximation is not always fine enough and can recognize counter examples. The first contribution of this thesis consist in characterizing by logical formulae, in an automatic way, what is a good approximation: an over-approximation which does not contain any counter example. Solving these formulae leads automatically to a good over-approximation if such an approximation exists, without any manual setting. An other problem of tree automata completion is the scaling when dealing with real life problems. In verification of Java programs using tree automata completion, this explosion may be due to the use of Peano numbers. The idea of the second contribution of this thesis is to evaluate directly the result of an arithmetic operation. Generally speaking, we integrate elements of an infinite domain in a tree automaton. Based on abstract interpretation, this thesis allows to integrate abstract lattice in tree automata. Operations on infinite domain are computed in one step of evaluation instead of probably many application of rewrite rules. Thus we adapted tree automata completion to this new type of tree automata with lattice, and genericity of the new algorithm allows to integrate many types of lattices. This ...