Low-Level Bi-Abduction

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F22%3APU144757" target="_blank" >RIV/00216305:26230/22:PU144757 - isvavai.cz</a>

Výsledek na webu

<a href="https://drops.dagstuhl.de/opus/volltexte/2022/16247/" target="_blank" >https://drops.dagstuhl.de/opus/volltexte/2022/16247/</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.ECOOP.2022.19" target="_blank" >10.4230/LIPIcs.ECOOP.2022.19</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Low-Level Bi-Abduction

Popis výsledku v původním jazyce

The paper proposes a new static analysis designed to handle open programs, i.e., fragments of programs, with dynamic pointer-linked data structures in particular, various kinds of lists that employ advanced low-level pointer operations. The goal is to allow such programs be analysed without a need of writing analysis harnesses that would first initialise the structures being handled. The approach builds on a special flavour of separation logic and the approach of bi-abduction. The code of interest is analyzed along the call tree, starting from its leaves, with each function analysed just once without any call context, leading to a set of contracts summarizing the behaviour of the analysed functions. In order to handle the considered programs, methods of abduction existing in the literature are significantly modified and extended in the paper. The proposed approach has been implemented in a tool prototype and successfully evaluated on not large but complex programs.

Název v anglickém jazyce

Low-Level Bi-Abduction

Popis výsledku anglicky

The paper proposes a new static analysis designed to handle open programs, i.e., fragments of programs, with dynamic pointer-linked data structures in particular, various kinds of lists that employ advanced low-level pointer operations. The goal is to allow such programs be analysed without a need of writing analysis harnesses that would first initialise the structures being handled. The approach builds on a special flavour of separation logic and the approach of bi-abduction. The code of interest is analyzed along the call tree, starting from its leaves, with each function analysed just once without any call context, leading to a set of contracts summarizing the behaviour of the analysed functions. In order to handle the considered programs, methods of abduction existing in the literature are significantly modified and extended in the paper. The proposed approach has been implemented in a tool prototype and successfully evaluated on not large but complex programs.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

36th European Conference on Object-Oriented Programming (ECOOP 2022)

ISBN

978-3-95977-225-9

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

30

Strana od-do

1-30

Název nakladatele

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Místo vydání

Wadern

Místo konání akce

Berlin

Datum konání akce

6. 6. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—