Tree Constraint Solver (TCS) - Linear tree inequality solver for superlinear resource bounds on Java programs

• Applicant: Dr. Sabine Bauer
• Subject Area: Theoretical Computer Science
• Term: from 2019 to 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 432878302

This project aims to provide provably correct upper bounds on the resource consumption of unannotated object-oriented Java programs. Such automatic resource analysis has become increasingly popular with considerable industrial interest but was hitherto mostly confined to functional programs and classical imperative programs with arrays as the only essential data structure. We build upon the well-established framework of type-based amortized analysis, which has been applied to functional programming languages with great success. Object-oriented programming poses several new challenges: a) data structures are implicitly defined through classes, but not explicitly given as in functional datatype declarations, b) imperative updates may lead to complex aliasing, c) more general data structures like doubly-linked lists, or even general graphs are possible. In earlier work, these challenges were addressed with a reduction from the resource bound question to an innovative constraint system involving infinitely many numerical variables (”linear tree constraints (LTC)”). However, the heuristic constraint solver that was presented there was limited to certain special cases. In very recent work, it was shown that the general LTC are decidable and thus might be also tractable in practice and the aim of this project is to explore this in detail. Concretely, we will develop and implement an efficient solution algorithm for general LTC that delivers also concrete upper bounds on the heap space consumption of programs. For that, decidability alone is not sufficient, we also need to detect minimal solutions to the constraints in terms of closed formulas. Further, we will determine and prove the exact complexity of the decision problem and find a new, better algorithm that falls into this complexity class. The decidability result obtained by now is a good starting point that makes the plan likely to work out.We will then use these results to design a type-based amortized resource analysis for imperative object-oriented programs and test it on a variety of example programs with a prototype implementation based on Java syntax.

• DFG Programme: Research Grants