Reachability analysis of term rewriting systems with Timbuk. (English) Zbl 1275.68083
Nieuwenhuis, Robert (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 8th international conference, LPAR 2001, Havana, Cuba, December 3–7, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42957-3/pbk). Lecture Notes in Computer Science 2250. Lecture Notes in Artificial Intelligence, 695-706 (2001).
Summary: We present Timbuk – a tree automata library – which implements usual operations on tree automata as well as a completion algorithm used to compute an over-approximation of the set of descendants \(\mathcal R^*(E)\) for a regular set \(E\) and a term rewriting system \(\mathcal R\), possibly non-linear and non-terminating. On several examples of term rewriting systems representing programs and systems to verify, we show how to use Timbuk to construct their approximations and then prove unreachability properties of these systems.
For the entire collection see [Zbl 1046.03001].
For the entire collection see [Zbl 1046.03001].
