Detail publikace

From Shapes to Amortized Complexity

FIEDOR, T. HOLÍK, L. ROGALEWICZ, A. VOJNAR, T. SINN, M. ZULEGER, F.

Originální název

From Shapes to Amortized Complexity

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

We propose a new method for the automated resource bound analysis of programs manipulating dynamic data structures built on top of an underlying shape and resource bound analysis. Our approach first constructs an integer abstraction for the input program using information gathered by a shape analyser; then a resource bound analyzer is run on the resulting integer program. The integer abstraction is based on shape norms-numerical measures on dynamic data structures (e.g., the length of a linked list). In comparison to related approaches, we consider a larger class of shape norms which we derive by a lightweight program analysis. The analysis identifies paths through the involved dynamic data structures, and filters the norms which are unlikely to be useful for the later bound analysis. We present a calculus for deriving the numeric changes of the shape norms, thereby generating the integer program. Our calculus encapsulates the minimal information which is required from the shape analysis. We have implemented our approach on top of the Forester shape analyser and evaluated it on a number of programs manipulating various list and tree structures using the Loopus tool as the underlying bounds analyser. We report on programs with complex data structures and/or using complex algorithms that could not be analysed in a fully automated and precise way before.

Klíčová slova

program analysis, shape analysis, forest automata, tree automata, resource bounds analysis, amortized complexity

Autoři

FIEDOR, T.; HOLÍK, L.; ROGALEWICZ, A.; VOJNAR, T.; SINN, M.; ZULEGER, F.

Vydáno

7. 1. 2018

Nakladatel

Springer Verlag

Místo

Heidelberg

ISBN

978-3-319-73720-1

Kniha

Proceedings of VMCAI'18

Edice

Lecture Notes in Computer Science

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Ročník

10145

Číslo

10747

Stát

Spolková republika Německo

Strany od

205

Strany do

225

Strany počet

21

URL

https://link.springer.com/chapter/10.1007%2F978-3-319-73721-8_10

BibTex

@inproceedings{BUT144484,
  author="Tomáš {Fiedor} and Lukáš {Holík} and Adam {Rogalewicz} and Tomáš {Vojnar} and Moritz {Sinn} and Florian {Zuleger}",
  title="From Shapes to Amortized Complexity",
  booktitle="Proceedings of VMCAI'18",
  year="2018",
  series="Lecture Notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  volume="10145",
  number="10747",
  pages="205--225",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-319-73721-8\{_}10",
  isbn="978-3-319-73720-1",
  issn="0302-9743",
  url="https://link.springer.com/chapter/10.1007%2F978-3-319-73721-8_10"
}