Abstract
Term rewriting systems are now commonly used as a modeling language for programs or systems. On 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. For disproving reachability (i.e. proving non reachability of a term) on non terminating and non confluent rewriting models, Knuth-Bendix completion and other usual rewriting techniques do not apply. Using the tree automaton completion technique, it has been shown that the non reachability of a term t can be shown by computing an over-approximation of the set of reachable terms and prove that t is not in the over-approximation. However, when the term t is in the approximation, nothing can be said.
In this paper, we improve this approach as follows: given a term t, we try to compute an over-approximation which does not contain t by using an approximation refinement that we propose. If the approximation refinement fails then t is a reachable term. This semi-algorithm has been prototyped in the Timbuk tool. We present some experiments with this prototype showing the interest of such an approach w.r.t. verification on rewriting models.
This work has been funded by the French ANR-06-SETI-014 RAVAJ project.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Boichut, Y., Genet, T., Jensen, T., Le Roux, L.: Rewriting approximations for fast prototyping of static analyzers. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 48–62. Springer, Heidelberg (2007)
Boichut, Y., Héam, P.-C.: A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations. Information Processing Letters ( to appear, 2008)
Boichut, Y., Héam, P.-C., Kouchnarenko, O.: Automatic Verification of Security Protocols Using Approximations. Technical Report RR-5727, INRIA (2005)
Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking. In: proceedings of INFINITY. BRICS Notes Series, vol. 4, pp. 15–24 (2005)
Clarke, E.: Counterexample-guided abstraction refinement. In: proceedings of TIME (2003)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Clarke, E.M., Lu, Y., Jha, S., Veith, H.: Tree-like counterexamples in model checking. In: proceedings of LICS, pp. 19–29 (2002)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2002)
Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517. Springer, Heidelberg (2002)
Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems. In: Handbook of Theoretical Computer Science, vol. B, ch.6, pp. 244–320. Elsevier Science Publishers B. V (1990)
Feuillade, G., Genet, T., VietTriemTong, V.: Reachability analysis over term rewriting systems. Journal of Automated Reasonning 33(3-4) (2004)
Genet, T., Klay, F.: Rewriting for Cryptographic Protocol Verification. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 271–290. Springer, Heidelberg (2000)
Genet, T., Tong, V.V.T.: Reachability Analysis of Term Rewriting Systems with timbuk. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 691–702. Springer, Heidelberg (2001)
Gilleron, R., Tison, S.: Regular tree languages and rewrite systems. Fundamenta Informatica 24(1/2), 157–174 (1995)
Gyenizse, P., Vágvölgyi, S.: Linear Generalized Semi-Monadic Rewrite Systems Effectively Preserve Recognizability. Theoretical Computer Science 194(1-2), 87–122 (1998)
Jacquemard, F.: Decidable approximations of term rewriting systems. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 362–376. Springer, Heidelberg (1996)
Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental Verification by Abstraction. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031. Springer, Heidelberg (2001)
Monniaux, D.: Abstracting cryptographic protocols with tree automata. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694. Springer, Heidelberg (1999)
Takai, T., Kaji, Y., Seki, H.: Right-linear finite-path overlapping term rewriting systems effectively preserve recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boichut, Y., Courbis, R., Héam, PC., Kouchnarenko, O. (2008). Finer Is Better: Abstraction Refinement for Rewriting Approximations. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-70590-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70588-8
Online ISBN: 978-3-540-70590-1
eBook Packages: Computer ScienceComputer Science (R0)