Name
Abstract | ||
|---|---|---|
Term Rewriting Systems (TRSs) are now commonly used as a modeling language for applications. In those rewriting based models, reachability analysis, i.e. proving or disproving that a given term is reachable from a set of input terms, provides an efficient verification technique. Using a tree automata completion technique, it has been shown that the non reachability of a term tcan be verified by computing an over-approximation of the set of reachable terms and proving that tis not in the over-approximation. Since the verification of real programs gives rise to rewrite models of significant size, efficient implementations of completion are essential. We present in this paper a TRS transformation preserving the reachability analysis by tree automata completion. This transformation makes the completion implementation based on rewriting techniques possible. Thus, the reduction of a term to a state by a tree automaton is fully handled by rewriting. This approach has been prototyped in Tom, a language extension which adds rewriting primitives to Java. The first experiments are very promising relative to the state-of-the-art tool Timbuk. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-79980-1_6 | AMAST |
Keywords | Field | DocType |
efficient implementation,tree automata completion technique,reachability analysis,reachable term,non reachability,tree automata completion,trs transformation,input term,tree automaton,completion implementation,modeling language | Programming language,Computer science,Automaton,Modeling language,Theoretical computer science,Reachability,Critical pair,Confluence,Rewriting,Tree automaton,Knuth–Bendix completion algorithm | Conference |
Volume | ISSN | Citations |
5140 | 0302-9743 | 8 |
PageRank | References | Authors |
0.46 | 15 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Emilie Balland | 1 | 233 | 14.22 |
| Yohan Boichut | 2 | 67 | 5.58 |
| Thomas Genet | 3 | 310 | 16.76 |
| Pierre-etienne Moreau | 4 | 598 | 40.40 |