In this paper, we present Tree Data Decision Diagrams, a compact data structure of symbolic verification based on term rewriting systems. By this way, we can benefit termination researches in term rewriting systems to improve the model-checking quality. Our experimental implementation uses tree automata technique that provides the capability to maintain the internal representation of data in canonical form.
Content
Author and article information
Contributors
Jean-Michel COUVREUR
Conference
Publication date:
July
2008
Publication date
(Print):
July
2008
Pages: 1-11
Affiliations
[0001]LIFO (Laboratoire d’Informatique Fondamentale d’Orléans)
University of Orleans
Léonard de Vinci street B.P. 6759, F-45067 ORLEANS Cedex 2
http://www.univ-orleans.fr/lifo/