Template-Based Verification of Array-Manipulating Programs

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F24%3APU154983" target="_blank" >RIV/00216305:26230/24:PU154983 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007/978-3-031-56222-8_12" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-031-56222-8_12</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-56222-8_12" target="_blank" >10.1007/978-3-031-56222-8_12</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Template-Based Verification of Array-Manipulating Programs

Popis výsledku v původním jazyce

This work deals with the 2LS program verification framework that combines several verification techniques-namely, abstract domains, templated invariants, k-induction, bounded model checking, and SAT/SMT solving. A distinguishing feature of the approach used by 2LS is that it allows for seamless combinations of various program abstractions. In this work, we introduce a novel abstract template domain allowing 2LS to reason about arrays, using an arbitrary abstract domain to describe values that are stored inside the arrays (including nested arrays and dynamic linked data structures), and with the arrays possibly nested inside other structures. The approach uses array index expressions to split each array into multiple contiguous, non-overlapping segments and computes a different invariant for each of them. We illustrate the approach on a program dealing with a list of arrays and subsequently present how the new domain allowed 2LS to improve in the international software verification competition SV-COMP.

Název v anglickém jazyce

Template-Based Verification of Array-Manipulating Programs

Popis výsledku anglicky

This work deals with the 2LS program verification framework that combines several verification techniques-namely, abstract domains, templated invariants, k-induction, bounded model checking, and SAT/SMT solving. A distinguishing feature of the approach used by 2LS is that it allows for seamless combinations of various program abstractions. In this work, we introduce a novel abstract template domain allowing 2LS to reason about arrays, using an arbitrary abstract domain to describe values that are stored inside the arrays (including nested arrays and dynamic linked data structures), and with the arrays possibly nested inside other structures. The approach uses array index expressions to split each array into multiple contiguous, non-overlapping segments and computes a different invariant for each of them. We illustrate the approach on a program dealing with a list of arrays and subsequently present how the new domain allowed 2LS to improve in the international software verification competition SV-COMP.

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

<a href="/cs/project/GA23-06506S" target="_blank" >GA23-06506S: Pokročilá analýza a verifikace pro pokročilý software</a><br>

Návaznosti

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

Rok uplatnění

2024

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

Taming the Infinities of Concurrency

ISBN

978-3-031-56221-1

ISSN

—

e-ISSN

—

Počet stran výsledku

19

Strana od-do

206-224

Název nakladatele

Springer Nature Switzerland AG

Místo vydání

Cham

Místo konání akce

Centre for Security, Reliability and Trust (SnT)

Datum konání akce

6. 4. 2024

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

WRD - Celosvětová akce

Kód UT WoS článku

001215137000011