Skip to Main content Skip to Navigation

Regions and Permissions for Verifying Data Invariants

Romain Bardou 1, * Claude Marché 2
* Corresponding author
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : To formally verify behavioral properties of programs, stating complex first-order formulas as data invariants proves useful. In the context of pointer programs, such invariants are hard to maintain because of aliasing. We propose a type system based on memory regions and linear permissions which allows to reduce preservation of invariants to first-order verification conditions in a sound way. It further allows data abstraction and effect hiding. It thus provides an approach to modular verification of behavioral properties of pointer programs.
Complete list of metadatas

Cited literature [29 references]  Display  Hide  Download
Contributor : Claude Marché <>
Submitted on : Monday, October 11, 2010 - 5:01:44 PM
Last modification on : Tuesday, April 21, 2020 - 1:07:37 AM
Document(s) archivé(s) le : Thursday, October 25, 2012 - 4:51:11 PM


Files produced by the author(s)


  • HAL Id : inria-00525384, version 1



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



Record views


Files downloads