Skip to Main content Skip to Navigation
Conference papers

Data Abstraction: A General Framework to Handle Program Verification of Data Structures

Abstract : Proving properties on programs accessing data structures such as arrays often requires universally quantified invariants, e.g., "all elements below index i are nonzero". In this article, we propose a general data abstraction scheme operating on Horn formulas, into which we recast previously published abstractions. We show that our instantiation scheme is relatively complete: the generated purely scalar Horn clauses have a solution (inductive invariants) if and only if the original problem has one expressible by the abstraction.
Complete list of metadata

https://hal.inria.fr/hal-03321868
Contributor : Laure Gonnord Connect in order to contact the contributor
Submitted on : Wednesday, August 18, 2021 - 1:27:50 PM
Last modification on : Monday, May 16, 2022 - 3:06:02 PM
Long-term archiving on: : Friday, November 19, 2021 - 6:13:30 PM

File

braine_al_sas2021.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Julien Braine, Laure Gonnord, David Monniaux. Data Abstraction: A General Framework to Handle Program Verification of Data Structures. SAS 2021 - 28th Static Analysis Symposium, Oct 2021, Chicago, United States. pp.215-235, ⟨10.1007/978-3-030-88806-0_11⟩. ⟨hal-03321868⟩

Share

Metrics

Record views

91

Files downloads

119