A completion algorithm for lattice tree automata

Thomas Genet 1, 2 Tristan Le Gall 3 Axel Legay 1, 4 Valérie Murat 1, 2
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
4 TRISKELL - Reliable and efficient component based software engineering
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : When dealing with infinite-state systems, Regular Tree Model Checking approaches may have some difficulties to represent infinite sets of data. We propose Lattice Tree Automata, an extended version of tree automata to represent complex data domains and their related operations in an efficient manner. Moreover, we introduce a new completion-based algorithm for computing the possibly infinite set of reachable states in a finite amount of time. This algorithm is independent of the lattice making it possible to seamlessly plug abstract domains into a Regular Tree Model Checking algorithm. As a first instance, we implemented a completion with an interval abstract domain. We provide some experiments showing that this implementation permits to scale up regular tree model-checking of Java programs dealing with integer arithmetics.
Document type :
Conference papers
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01834984
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:34 AM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Links full text

Identifiers

Citation

Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat. A completion algorithm for lattice tree automata. CIAA 2013 - 18th International Conference on Implementation and Application of Automata, Jul 2013, Halifax, NS, Canada. pp.134-145, ⟨10.1007/978-3-642-39274-0_13⟩. ⟨cea-01834984⟩

Share

Metrics

Record views

315