Abstract
We present a technique for approximating the set of reachable terms of a given term rewriting system starting from a given initial regular set of terms. The technique is based on previous work by other authors with the same goal, and yields a finite tree automaton recognising an over-approximation of the set of reachable terms. Our contributions are, firstly, to use Horn clauses to specify the transitions of a possibly infinite-state tree automaton defining (at least) the reachable terms. Apart from being a clear specification, the Horn clause model is the basis for further automatic approximations using standard logic program analysis techniques, yielding finite-state tree automata. The approximations are applied in two stages: first a regular approximation of the model of the given Horn clauses is constructed, and secondly a more precise relational abstraction is built using the first approximation. The analysis uses efficient representations based on BDDs, leading to more scalable implementations. We report on preliminary experimental results.
Work supported by the Danish Natural Science Research Council project SAFT: Static Analysis Using Finite Tree Automata.
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.
Similar content being viewed by others
References
Balland, E., Boichut, Y., Moreau, P.-E., Genet, T.: Towards an efficient implementation of tree automata completion. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 67–82. Springer, Heidelberg (2008)
Boichut, Y., Genet, T., Jensen, T.P., Roux, L.L.: Rewriting approximations for fast prototyping of static analyzers. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 48–62. Springer, Heidelberg (2007)
Boulanger, D., Bruynooghe, M.: A systematic construction of abstract domains. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 61–77. Springer, Heidelberg (1994)
Boulanger, D., Bruynooghe, M., Denecker, M.: Abstracting s-semantics using a model-theoretic approach. In: Hermenegildo, M., Penjam, J. (eds.) PLILP 1994. LNCS, vol. 844, pp. 432–446. Springer, Heidelberg (1994)
Bruynooghe, M., Janssens, G.: An instance of abstract interpretation integrating type and mode inferencing. In: Kowalski, R., Bowen, K. (eds.) Proceedings of ICLP/SLP, pp. 669–683. MIT Press, Cambridge (1988)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (1999), http://www.grappa.univ-lille3.fr/tata
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 238–252 (1977)
Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of Theoretical Computer Science, Formal Models and Semantics, vol B, pp. 243–320. Elsevier and MIT Press (1990)
Feuillade, G., Genet, T., Tong, V.V.T.: Reachability analysis over term rewriting systems. J. Autom. Reasoning 33(3-4), 341–383 (2004)
Frühwirth, T., Shapiro, E., Vardi, M., Yardeni, E.: Logic programs as types for logic programs. In: Proceedings of the IEEE Symposium on Logic in Computer Science, Amsterdam (July 1991)
Gallagher, J.P., Boulanger, D., Sağlam, H.: Practical model-based static analysis for definite logic programs. In: Lloyd, J.W. (ed.) Proc. of International Logic Programming Symposium, pp. 351–365. MIT Press, Cambridge (1995)
Gallagher, J.P., de Waal, D.: Fast and precise regular approximation of logic programs. In: Van Hentenryck, P. (ed.) Proceedings of the International Conference on Logic Programming (ICLP 1994), Santa Margherita Ligure. MIT Press (1994)
Gallagher, J.P., Henriksen, K.S.: Abstract domains based on regular types. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 27–42. Springer, Heidelberg (2004)
Gallagher, J.P., Henriksen, K.S., Banda, G.: Techniques for scaling up analyses based on pre-interpretations. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 280–296. Springer, Heidelberg (2005)
Gallagher, J.P., Puebla, G.: Abstract interpretation over non-deterministic finite tree automata for set-based analysis of logic programs. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol. 2257. Springer, Heidelberg (2002)
Genet, T., Tong, V.V.T.: Reachability analysis of term rewriting systems with timbuk. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS, vol. 2250, pp. 695–706. Springer, Heidelberg (2001)
Heintze, N., Jaffar, J.: A Finite Presentation Theorem for Approximating Logic Programs. In: Proceedings of the 17th Annual ACM Symposium on Principles of Programming Languages, pp. 197–209. ACM Press, San Francisco (1990)
Horiuchi, K., Kanamori, T.: Polymorphic type inference in Prolog by abstract interpretation. In: Proc. 6th Conference on Logic Programming. LNCS, vol. 315, pp. 195–214. Springer, Heidelberg (1987)
Jacquemard, F.: Decidable approximations of term rewriting systems. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 362–376. Springer, Heidelberg (1996)
Jones, N.: Flow analysis of lazy higher order functional programs. In: Abramsky, S., Hankin, C. (eds.) Abstract Interpretation of Declarative Languages, Ellis-Horwood (1987)
Jones, N.D., Andersen, N.: Flow analysis of lazy higher-order functional programs. Theor. Comput. Sci. 375(1-3), 120–136 (2007)
Lloyd, J.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987)
Mishra, P.: Towards a theory of types in Prolog. In: Proceedings of the IEEE International Symposium on Logic Programming (1984)
Reynolds, J.C.: Automatic construction of data set definitions. In: Morrell, J. (ed.) Information Processing, vol. 68, pp. 456–461. North-Holland, Amsterdam (1969)
Ullman, J.: Principles of Knowledge and Database Systems, vol. 1. Computer Science Press (1988)
Van Hentenryck, P., Cortesi, A., Le Charlier, B.: Type analysis of Prolog using type graphs. Journal of Logic Programming 22(3), 179–210 (1994)
Vaucheret, C., Bueno, F.: More precise yet efficient type inference for logic programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 102–116. Springer, Heidelberg (2002)
Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: Pugh, W., Chambers, C. (eds.) PLDI, pp. 131–144. ACM, New York (2004)
Whaley, J., Unkel, C., Lam, M.S.: A bdd-based deductive database for program analysis (2004), http://bddbddb.sourceforge.net/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gallagher, J.P., Rosendahl, M. (2008). Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation . In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_47
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_47
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)