<div class="csl-bib-body">
<div class="csl-entry">Sextl, F., Rogalewicz, A., Vojnar, T., & Zuleger, F. (2025, January 21). <i>Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)</i> [Conference Presentation]. Theory and Practice of Static Analysis 2025, Denver, Colorado, United States of America (the). http://hdl.handle.net/20.500.12708/212815</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/212815
-
dc.description.abstract
Biabduction-based shape analysis verifies memory safety of open programs in an efficient compositional way and is applicable even for code fragments without a need for modelling their environment. Nevertheless, the technique suffers from two fundamental problems that were already described upon its introduction by Calcagno et al. (2009), namely dealing with unsound abduction results in indeterminately branching code and with unsound over-approximation within loop acceleration. Together, these problems facilitate the need for a second analysis phase to filter out unsound pre-conditions. In contrast, we introduce novel techniques that overcome the two problems and compute sound analysis results within a single analysis phase.
en
dc.language.iso
en
-
dc.subject
Biabduction
en
dc.subject
Shape Analysis
en
dc.subject
Separation Logic
en
dc.title
Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration (Extended Abstract)
en
dc.type
Presentation
en
dc.type
Vortrag
de
dc.contributor.affiliation
Brno University of Technology, Czechia
-
dc.contributor.affiliation
Masaryk University, Czechia
-
dc.type.category
Conference Presentation
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.author.orcid
0009-0003-5839-0726
-
tuw.author.orcid
0000-0002-7911-0549
-
tuw.author.orcid
0000-0002-2746-8792
-
tuw.author.orcid
0000-0003-1468-8398
-
tuw.event.name
Theory and Practice of Static Analysis 2025
en
dc.description.sponsorshipexternal
Czech Science Foundation
-
dc.description.sponsorshipexternal
Brno University of Technology, Faculty of Information Technology
-
dc.description.sponsorshipexternal
Horizon Europe
-
dc.description.sponsorshipexternal
Horizon 2020
-
dc.relation.grantnoexternal
23-06506S
-
dc.relation.grantnoexternal
FIT-S-23-8151
-
dc.relation.grantnoexternal
101160022
-
dc.relation.grantnoexternal
101034440
-
tuw.event.startdate
21-01-2025
-
tuw.event.enddate
21-01-2025
-
tuw.event.online
Hybrid
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Denver, Colorado
-
tuw.event.country
US
-
tuw.event.presenter
Sextl, Florian
-
tuw.presentation.online
Online
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.openairetype
conference paper not in proceedings
-
item.cerifentitytype
Publications
-
item.grantfulltext
none
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_18cp
-
item.fulltext
no Fulltext
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
Brno University of Technology
-
crisitem.author.dept
Masaryk University
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
