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.