Template-Based Verification of Array-Manipulating Programs
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Template-Based Verification of Array-Manipulating Programs
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA23-06506S" target="_blank" >GA23-06506S: Advanced Analysis and Verification for Advanced Software</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2024
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Taming the Infinities of Concurrency
ISBN
978-3-031-56221-1
ISSN
—
e-ISSN
—
Number of pages
19
Pages from-to
206-224
Publisher name
Springer Nature Switzerland AG
Place of publication
Cham
Event location
Centre for Security, Reliability and Trust (SnT)
Event date
Apr 6, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
001215137000011