Data Abstraction: A General Framework to Handle Program Verification of Data Structures
| Autor: | Laure Gonnord, Julien Braine, David Monniaux |
|---|---|
| Přispěvatelé: | CASH - Compilation and Analysis, Software and Hardware (CASH), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS), 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, ANR-17-CE23-0004,CODAS,Ordonnancement de programmes à structures de données complexes(2017), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), École normale supérieure de Lyon (ENS de Lyon), Laboratoire de l'Informatique du Parallélisme (LIP), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), École normale supérieure - Lyon (ENS Lyon), This work was partially supported by the ANR CODAS Project. |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Scheme (programming language)
Theoretical computer science Horn clause Computer science [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS] 02 engineering and technology Data Structures [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] Program analysis Clauses de Horn 0202 electrical engineering electronic engineering information engineering Abstraction Analyse de Programmes Horn Clauses computer.programming_language Program Analysis Scalar (physics) 020207 software engineering Static analysis Data structure 020202 computer hardware & architecture TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES If and only if TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Abstractions Computer Science::Programming Languages computer Structures de données |
| Zdroj: | [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 Static Analysis ISBN: 9783030888053 SAS SAS 2021-28th Static Analysis Symposium SAS 2021-28th Static Analysis Symposium, Oct 2021, Chicago, United States. pp.215-235, ⟨10.1007/978-3-030-88806-0_11⟩ HAL |
| DOI: | 10.1007/978-3-030-88806-0_11⟩ |
| Popis: | 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.; Pour prouver des propriétés de programmes qui manipulent des structures de données comme des tableaux , nous avons besoin de savoir résoudre des formules comportant des quantificateurs universels: par exemple, “tous les éléments d’index inférieur à $i$ sont différents de 0”. Dans ce rapport de recherche, nous proposons une technique générale d’abstraction opérant sur des Clauses de Horn, qui permet de reformuler un certain nombre d’abstractions déjà publiées. Nous montrons que notre schéma d’abstraction est relativement complet: le système de clauses purement scalaires a une solution (sous forme d’invariants inductifs) si et seulement si le problème initial a une solution exprimable dans la logique de l’abstraction. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|