Regions and Permissions for Verifying Data Invariants

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.Les invariants de données sont nécessaires pour établir des propriétés fonctionnelles avancées des programmes. Leur vérification par preuve demande de les exprimer dans un langage logique expressif comme les formules du premier ordre. Dans le cas des programmes avec pointeurs, la vérification de ces invariants est rendue encore plus complexe à cause du partage. Nous proposons un système de typage statique basé sur des régions mémoire et des permissions d'accès linéaires, afin de réduire, de façon sure, la vérifaction de preservation des invariants à des obligations de preuve. Notre approche permet l'abstraction de données et le masquage des effets de bords internes aux modules de programmes. Ainsi, cette approche est une méthode de vérification modulaire de propriétés de programmes avec pointeurs et partage