Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/inria-00525384
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

File

RR-7412.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

318

Files downloads

197