Regions and Permissions for Verifying Data Invariants

Romain Bardou 1, * Claude Marché 2
* Auteur correspondant
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Résumé : Les invariants de données sont nécessaires pour établir des propriétés fonctionnelles avancées des programmes. Leur vérification par preuve demande de les exprimer dans un langage logique expressif comme les formules du premier ordre. Dans le cas des programmes avec pointeurs, la vérification de ces invariants est rendue encore plus complexe à cause du partage. Nous proposons un système de typage statique basé sur des régions mémoire et des permissions d'accès linéaires, afin de réduire, de façon sure, la vérifaction de preservation des invariants à des obligations de preuve. Notre approche permet l'abstraction de données et le masquage des effets de bords internes aux modules de programmes. Ainsi, cette approche est une méthode de vérification modulaire de propriétés de programmes avec pointeurs et partage.
Type de document :
Rapport
[Research Report] RR-7412, INRIA. 2010, pp.40
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00525384
Contributeur : Claude Marché <>
Soumis le : lundi 11 octobre 2010 - 17:01:44
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : jeudi 25 octobre 2012 - 16:51:11

Fichier

RR-7412.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00525384, version 1

Collections

Citation

Romain Bardou, Claude Marché. Regions and Permissions for Verifying Data Invariants. [Research Report] RR-7412, INRIA. 2010, pp.40. 〈inria-00525384〉

Partager

Métriques

Consultations de la notice

251

Téléchargements de fichiers

98