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
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 : Thursday, April 5, 2018 - 12:30:08 PM
Long-term archiving on : 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

277

Files downloads

113