Skip to Main content Skip to Navigation

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

Julien Braine 1 Laure Gonnord 1 David Monniaux 2 
1 CASH - CASH - Compilation and Analysis, Software and Hardware
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
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 research report, we propose a general data abstraction scheme operating on Horn formulas, into which we recast previously published abstractions. We show 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
Contributor : Laure Gonnord Connect in order to contact the contributor
Submitted on : Wednesday, August 18, 2021 - 1:24:10 PM
Last modification on : Monday, May 16, 2022 - 3:06:02 PM


Files produced by the author(s)


  • HAL Id : hal-03214475, version 2



Julien Braine, Laure Gonnord, David Monniaux. Data Abstraction: A General Framework to Handle Program Verification of Data Structures. [Research Report] RR-9408, Inria Grenoble Rhône-Alpes; VERIMAG UMR 5104, Université Grenoble Alpes, France; LIP - Laboratoire de l’Informatique du Parallélisme; Université Lyon 1 - Claude Bernard; ENS Lyon. 2021, pp.1-29. ⟨hal-03214475v2⟩



Record views


Files downloads