Tree Schemata and Fair Termination

Laurent Mauborgne.
Tree Schemata and Fair Termination.
In J. Palsberg, editor, Static Analysis Symposium (SAS'00), volume 1824 of Lecture Notes in Computer Science, pages 302--320.
Springer-Verlag, 2000.
Compressed PostScript (123K), DVI (187K), PDF (295K).
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.

\bibitem{mauborgn00b}
{\sc Mauborgne, L.}
\newblock Tree schemata and fair termination.
\newblock In {\em Static Analyis Symposium (SAS'00)\/} (2000), J.~Palsberg,
  Ed., vol.~1824 of {\em Lecture Notes in Computer Science},
  Springer-Verlag, pp.~302--320.

@inproceedings{mauborgn00b,
author = "Laurent Mauborgne",
title = "Tree Schemata and Fair Termination",
booktitle = "Static Analyis Symposium (SAS'00)",
year = 2000,
volume = 1824,
editor = "J. Palsberg",
pages = "302--320",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag" }

Email: Laurent.Mauborgne@ens.fr