inria-00525384, version 1
Regions and Permissions for Verifying Data Invariants
Romain Bardou
a, 1Claude Marché
2
N° RR-7412 (2010)
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.
- a – Université Paris Sud - Paris XI
- 1: Laboratoire de Recherche en Informatique (LRI)
- CNRS : UMR8623 – Université Paris XI - Paris Sud
- 2: PROVAL (INRIA Saclay - Ile de France)
- INRIA – Université Paris XI - Paris Sud – CNRS : UMR
- Collaboration : INRIA Collaborative Research Action (ARC) ``CeProMi'' http://www.lri.fr/cepromi/
- Domain : Computer Science/Logic in Computer Science
- Keywords : Formal Specification – Deductive verification – Data invariants – Abstraction – Region-based type system
- Internal note : RR-7412
- inria-00525384, version 1
- http://hal.inria.fr/inria-00525384
- oai:hal.inria.fr:inria-00525384
- From: Claude Marché
- Submitted on: Monday, 11 October 2010 17:01:44
- Updated on: Friday, 5 November 2010 16:45:24
Associated documents
PDF : 
See also
Export