Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Monday, October 11, 2010 - 5:01:44 PM
Last modification on : Friday, October 28, 2022 - 3:28:37 AM
Long-term archiving on: : 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