Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2018 / Oberseminar / Sabine Bauer: A Decision Procedure for Linear Constraints over Infinite Trees


Inhaltsbereich

Sabine Bauer: A Decision Procedure for Linear Constraints over Infinite Trees

Oberseminarvortrag von Sabine Bauer über A Decision Procedure for Linear Constraints over Infinite Trees
Wann 11:00 12:00 05.07.2018
von bis
Wo Raum L109, Oettingenstr. 67
Termin übernehmen vCal
iCal

Es spricht Sabine Bauer über:
A Decision Procedure for Linear Constraints over Infinite Trees

Abstract:
We present recent results on a constraint satisfaction problem arising
from the inference of resource types in automatic amortized analysis
for object-oriented programs by Rodriguez and Hofmann. More precisely,
they gave a reduction from inference of resource types to constraint
solving. Thus, once we have found an algorithm to solve the
constraints generated from a program, we can read off the resource
consumption from their solutions. These constraints are essentially
linear inequalities between infinite trees of nonnegative rational
numbers which are added and compared pointwise. We study the question
of simultaneous satisfiability of a system of such constraints in two
variants with significantly different complexity. First, we show that
in its general form (which is the original formulation presented by
Hofmann and Rodriguez) this satisfiability problem is –- already in
the list case –- hard for the famous Skolem-Mahler-Lech problem
whose decidability status is still open but which is at least NP-hard.
We then identify a subcase of the problem that still covers all
instances arising from type inference in the aforementioned amortized
analysis and show decidability of satisfiability (in polynomial time
for lists) by a reduction to linear programming. This yields a
decision procedure that covers the entire range of constraints needed
for resource analysis.

Bemerkung: Dieser Vortrag ist eine kurze Darstellung meiner Arbeit,
wie ich sie auf einem Floc-Workshop übernächste Woche präsentieren
werde. D.h. manche von Euch werden den Inhalt schon kennen. Der
Vortrag ist als Übung gedacht und ich freue mich auf eure
Verbesserungsvorschläge und Feedback.

Artikelaktionen


Funktionsleiste