Decidable Linear Tree Constraints
Author: Sabine Bauer
Paper Information
Title: | Decidable Linear Tree Constraints |
Authors: | Sabine Bauer |
Proceedings: | LaSh AllTalks |
Editor: | David Mitchell |
Keywords: | Linear Tree Constraints, Decision Procedures, Program Analysis |
Abstract: | ABSTRACT. Linear constraints on infinite trees arise in object-oriented resource analysis, when inferring resource types for programs similar to (a fragment of) Java. These types encode the heap space usage of programs, and one can calculate an upper bound on it using the constraint solutions. I will explain the logic and the meaning of the constraints with examples and briefly describe their role in program analysis. I then focus on the decision procedures for both list and tree constraints. After presenting the ideas for the list case, I will generalize them to trees and point out the difficulties that appear there and how they are treated. |
Pages: | 1 |
Talk: | Jul 18 17:15 (Session 129E: Modelling and Solving) |
Paper: |