Abstract
We present a new representation for possibly infinite sets of possibly infinite trees. This representation makes extensive use of sharing to achieve efficiency. As much as possible, equivalent substructures are stored in the same place. The new representation is based on a first approximation of the sets which has this uniqueness property. This approximation is then refined using powerful representations of possibly infinite relations. The result is a representation which can be used for practical analysis using abstract interpretation techniques. It is more powerful than traditional techniques, and deals well with approximation strategies. We show on a simple example, fair termination, how the expressiveness of the representation can be used to obtain very simple and intuitive analysis.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aiken, A., Murphy, B.R.: Implementing regular tree expressions. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 427–446. Springer, Heidelberg (1991)
Andersen, N.: Approximating term rewriting systems with tree grammars. Technical Report 86/16, Institute of Datalogy, University of Copenhagen, (1986)
Biehl, M., Klarlund, N., Rauhe, T.: Algorithms for guided tree automata. In: Raymond, D.R., Yu, S., Wood, D. (eds.) WIA 1996. LNCS, vol. 1260, Springer, Heidelberg (1997)
Börstler, J., Möncke, U., Wilhelm, R.: Table compression for tree automata. ACM Transactions on Programming Languages and Systems 13(3), 295–314 (1991)
Bryant, R.E.: Graph based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35, 677–691 (1986)
Charatonik, W., Podelski, A.: Co-definite set constraints. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 211–225. Springer, Heidelberg (1998)
Cousot, P.: Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique des programmes. PhD thesis, Université de Grenoble, (March 1978)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixpoints. In: 4th ACM Symposium on Principles of Programming Languages (POPL 1977), pp. 238–252 (1977)
Cousot, P., Cousot, R.: Formal languages, grammar and setconstraint-based program analysis by abstract interpretation. In: Conference on Functional Programming and Computer Architecture (FPCA 1995), June 1995, pp. 170–181 (1995)
Devienne, P., Talbot, J., Tison, S.: Solving classes of set constraints with tree automata. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 62–76. Springer, Heidelberg (1997)
Francez, N.: Fairness. Texts and Monographs in Computer Science. Springer, Heidelberg (1986)
Gécseg, F., Steinby, M.: Tree Automata, Akadémia Kiadó (1984)
Heintze, N.: Set Based Program Analysis. PhD thesis, School of Computer Science, Carnegie Mellon University (October 1992)
Henriksen, J.G., Jensen, J., Jørgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, Springer, Heidelberg (1995)
Jones, N.D., Muchnick, S.S.: Flow analysis and optimization of LISP-like structures. In: 6th ACM Symposium on Principles of Programming Languages (POPL 1979), pp. 244–256. ACM Press, New York (January 1979)
Mauborgne, L.: Binary decision graphs. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 101–116. Springer, Heidelberg (1999)
Mauborgne, L.: Representation of Sets of Trees for Abstract Interpretation. PhD thesis, École Polytechnique, Palaiseau, France (November 1999)
Mauborgne, L.: Improving the representation of infinite trees to deal with sets of trees. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, p. 275. Springer, Heidelberg (2000) (to appear)
Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. CACM 19(5), 279–286 (1976)
Reynolds, J.: Automatic computation of data set definitions. In: Information Processing 1968, pp. 456–461. Elsevier Science Publisher, Amsterdam (1969)
Schwartzbach, M.I.: Infinite values in hierarchical imperative types. In: Arnold, A. (ed.) CAAP 1990. LNCS, vol. 431, pp. 254–268. Springer, Heidelberg (1990)
Sørensen, M.H.: A grammar-based data-flow analysis to stop deforestation. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, pp. 335–351. Springer, Heidelberg (1994)
Thatcher, J.W., Wright, J.B.: Generalized finite automata with an application to a decision problem of second-order logic. Mathematical Systems Theory 2, 57–82 (1968)
Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575–597. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mauborgne, L. (2000). Tree Schemata and Fair Termination. In: Palsberg, J. (eds) Static Analysis. SAS 2000. Lecture Notes in Computer Science, vol 1824. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45099-3_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-45099-3_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67668-3
Online ISBN: 978-3-540-45099-3
eBook Packages: Springer Book Archive