<div class="csl-bib-body">
<div class="csl-entry">Fiedor, T., Holík, L., Rogalewicz, A., Sinn, M., Vojnar, T., & Zuleger, F. (2018). From Shapes to Amortized Complexity. In <i>Verification, Model Checking, and Abstract Interpretation - 19th International , VMCAI 2018, Los Angeles, CA, USA, January 7-9, Proceedings ; Dillig, Isil; Palsberg, Jens</i>. Los Angeles. https://doi.org/10.1007/978-3-319-73721-8_10</div>
</div>
The final publication is available via <a href="https://doi.org/10.1007/978-3-319-73721-8_10" target="_blank">https://doi.org/10.1007/978-3-319-73721-8_10</a>.
-
dc.description.abstract
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.<br /><br />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.
en
dc.description.sponsorship
Austrian Science Funds (FWF) Austrian National Research Network (RiSE)
-
dc.description.sponsorship
Czech Science Foundation
-
dc.description.sponsorship
IT4Innovations Excellence in Science (IT4IXS)
-
dc.description.sponsorship
BUT FIT
-
dc.language
English
-
dc.language.iso
en
-
dc.publisher
Los Angeles
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.title
From Shapes to Amortized Complexity
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.relation.publication
Verification, Model Checking, and Abstract Interpretation - 19th International , VMCAI 2018, Los Angeles, CA, USA, January 7-9, Proceedings ; Dillig, Isil; Palsberg, Jens
-
dc.relation.isbn
9783319737201
-
dc.relation.grantno
S11403-N23
-
dc.relation.grantno
17-12465S
-
dc.relation.grantno
LQ1602
-
dc.relation.grantno
FIT-S-17-4014
-
dc.rights.holder
Springer International Publishing AG 2018
-
dc.type.category
Full-Paper Contribution
-
tuw.container.volume
10747
-
tuw.peerreviewed
true
-
tuw.version
am
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
tuw.publisher.doi
10.1007/978-3-319-73721-8_10
-
dc.identifier.libraryid
AC15093557
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:3-3626
-
tuw.author.orcid
0000-0003-1468-8398
-
dc.rights.identifier
Urheberrechtsschutz
de
dc.rights.identifier
In Copyright
en
item.languageiso639-1
en
-
item.grantfulltext
open
-
item.openaccessfulltext
Open Access
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.fulltext
with Fulltext
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E184 - Institut für Informationssysteme
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering