Tree Schemata and Fair Termination

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 l 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.

• Type: Conference
• Year: 2000
• Where: SAS
• Authors: Laurent Mauborgne
• Keywords: Approximation, Formal Methods, Infinite, Infinite Sets, SAS 2000