Compositional Shape Analysis with Shared Abduction and
Biabductive Loop Acceleration

D 2025

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration

SEXTL, Florian; Adam ROGALEWICZ; Tomáš VOJNAR a Florian ZULEGER

Základní údaje

Originální název

Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration

Autoři

SEXTL, Florian; Adam ROGALEWICZ; Tomáš VOJNAR a Florian ZULEGER

Vydání

Cham, Proc. of the 34th European Symposium on Programming – ESOP'25, od s. 230-257, 28 s. 2025

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

Associated technical report., URL

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-91120-0

DOI

https://doi.org/10.1007/978-3-031-91121-7_10

EID Scopus

2-s2.0-105004789856

Klíčová slova anglicky

program analysis;programs with pointers;low-level pointer manipulation;separation logic;biabduction;

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 14. 8. 2025 17:24, prof. Ing. Tomáš Vojnar, Ph.D.

Anotace

V originále

Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its usefulness, several open problems persist for this kind of analysis; two of which we address in this paper. On the one hand, the original analysis is path-sensitive but cannot combine safety requirements for related branches. This causes the analysis to require additional soundness checks and decreases the analysis’ precision. We extend the underlying symbolic execution and propose a framework for shared abduction where a common pre-condition is maintained for related computation branches. On the other hand, prior implementations lift loop acceleration methods from forward analysis to biabduction analysis by applying them separately on the pre- and post-condition, which can lead to imprecise or even unsound acceleration results that do not form a loop invariant. In contrast, we propose biabductive loop acceleration, which explicitly constructs and checks candidate loop invariants. For this, we also introduce a novel heuristic called shape extrapolation. This heuristic takes advantage of locality in the handling of list-like data structures (which are the most common data structures found in low-level code) and jointly accelerates pre- and post-conditions by extrapolating the related shapes. In addition to making the analysis more precise, our techniques also make biabductive analysis more efficient since they are sound in just one analysis phase. In contrast, prior techniques always require two phases (as the first phase can produce contracts that are unsound and must hence be verified). We experimentally confirm that our techniques improve on prior techniques; both in terms of precision and runtime of the analysis.

Návaznosti

GA23-06506S, projekt VaV

Název: Pokročilá analýza a verifikace pro pokročilý software

Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software

Citovat

SEXTL, Florian; Adam ROGALEWICZ; Tomáš VOJNAR a Florian ZULEGER. Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. In Proc. of the 34th European Symposium on Programming – ESOP'25. Cham: Springer, 2025, s. 230-257. ISBN 978-3-031-91120-0. Dostupné z: https://doi.org/10.1007/978-3-031-91121-7_10.

@inproceedings{2512080,
   author = {Sextl, Florian and Rogalewicz, Adam and Vojnar, Tomáš and Zuleger, Florian},
   address = {Cham},
   booktitle = {Proc. of the 34th European Symposium on Programming – ESOP'25},
   doi = {https://doi.org/10.1007/978-3-031-91121-7_10},
   keywords = {program analysis;programs with pointers;low-level pointer manipulation;separation logic;biabduction;},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-031-91120-0},
   pages = {230-257},
   publisher = {Springer},
   title = {Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration},
   url = {https://link.springer.com/chapter/10.1007/978-3-031-91121-7_10},
   year = {2025}
}

TY  - CONF
ID  - 2512080
AU  - Sextl, Florian - Rogalewicz, Adam - Vojnar, Tomáš - Zuleger, Florian
PY  - 2025
TI  - Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration
PB  - Springer
CY  - Cham
SN  - 9783031911200
KW  - program analysis;programs with pointers;low-level pointer manipulation;separation logic;biabduction;
UR  - https://link.springer.com/chapter/10.1007/978-3-031-91121-7_10
N2  - Biabduction-based shape analysis is a compositional verification and analysis technique that can prove memory safety in the presence of complex, linked data structures. Despite its usefulness, several open problems persist for this kind of analysis; two of which we address in this paper. On the one hand, the original analysis is path-sensitive but cannot combine safety requirements for related branches. This causes the analysis to require additional soundness checks and decreases the analysis’ precision. We extend the underlying symbolic execution and propose a framework for shared abduction where a common pre-condition is maintained for related computation branches. On the other hand, prior implementations lift loop acceleration methods from forward analysis to biabduction analysis by applying them separately on the pre- and post-condition, which can lead to imprecise or even unsound acceleration results that do not form a loop invariant. In contrast, we propose biabductive loop acceleration, which explicitly constructs and checks candidate loop invariants. For this, we also introduce a novel heuristic called shape extrapolation. This heuristic takes advantage of locality in the handling of list-like data structures (which are the most common data structures found in low-level code) and jointly accelerates pre- and post-conditions by extrapolating the related shapes. In addition to making the analysis more precise, our techniques also make biabductive analysis more efficient since they are sound in just one analysis phase. In contrast, prior techniques always require two phases (as the first phase can produce contracts that are unsound and must hence be verified). We experimentally confirm that our techniques improve on prior techniques; both in terms of precision and runtime of the analysis.
ER  -

SEXTL, Florian; Adam ROGALEWICZ; Tomáš VOJNAR a Florian ZULEGER. Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration. In \textit{Proc. of the 34th European Symposium on Programming – ESOP'25}. Cham: Springer, 2025, s.~230-257. ISBN~978-3-031-91120-0. Dostupné z: https://doi.org/10.1007/978-3-031-91121-7\_{}10.

Přehled o publikaci