Template-Based Verification of Array-Manipulating Programs

Template-Based Verification of Array-Manipulating Programs

Stať ve sborníku v databázi WoS či Scopus

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.

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.

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

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

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

2025

20.03.2024

Springer Nature Switzerland AG

Cham

978-3-031-56221-1

Taming the Infinities of Concurrency

Lecture Notes in Computer Science

14660

206

224

19

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