Detail publikace

Template-Based Verification of Array-Manipulating Programs

MALÍK, V. VOJNAR, T. SCHRAMMEL, P.

Originální název

Template-Based Verification of Array-Manipulating Programs

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

program analysis, formal verification, invariant inference, loop invariants, abstract interpretation, k-induction, loop unwinding, array abstract domain, array contents analysis

Autoři

MALÍK, V.; VOJNAR, T.; SCHRAMMEL, P.

Vydáno

20. 3. 2024

Nakladatel

Springer Nature Switzerland AG

Místo

Cham

ISBN

978-3-031-56221-1

Kniha

Taming the Infinities of Concurrency

Edice

Lecture Notes in Computer Science

Strany od

206

Strany do

224

Strany počet

19

URL

https://link.springer.com/chapter/10.1007/978-3-031-56222-8_12

BibTex

@inproceedings{BUT193768,
  author="Viktor {Malík} and Tomáš {Vojnar} and Peter {Schrammel}",
  title="Template-Based Verification of Array-Manipulating Programs",
  booktitle="Taming the Infinities of Concurrency",
  year="2024",
  series="Lecture Notes in Computer Science",
  volume="14660",
  pages="206--224",
  publisher="Springer Nature Switzerland AG",
  address="Cham",
  doi="10.1007/978-3-031-56222-8\{_}12",
  isbn="978-3-031-56221-1",
  url="https://link.springer.com/chapter/10.1007/978-3-031-56222-8_12"
}