Publication detail

Template-Based Verification of Array-Manipulating Programs

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

Original Title

Template-Based Verification of Array-Manipulating Programs

Type

conference paper

Language

English

Original Abstract

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.

Keywords

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

Authors

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

Released

20. 3. 2024

Publisher

Springer Nature Switzerland AG

Location

Cham

ISBN

978-3-031-56221-1

Book

Taming the Infinities of Concurrency

Edition

Lecture Notes in Computer Science

Pages from

206

Pages to

224

Pages count

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"
}