Publication Details
Template-Based Verification of Array-Manipulating Programs
program analysis, formal verification, invariant inference, loop invariants,
abstract interpretation, k-induction, loop unwinding, array abstract domain,
array contents analysis
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.
@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"
}