Data Abstraction: A General Framework to Handle Program Verification of Data Structures - IMAG Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

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

Résumé

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.
Fichier principal
Vignette du fichier
braine_al_sas2021.pdf (5.34 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03321868 , version 1 (18-08-2021)

Identifiants

Citer

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⟩
137 Consultations
190 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More