@techreport{bardou10rr, author = {Romain Bardou and Claude March\'e}, title = {Regions and Permissions for Verifying Data Invariants}, institution = {INRIA}, year = 2010, topics = {team}, hal = {http://hal.inria.fr/inria-00525384/en/}, note = {\url{http://hal.inria.fr/inria-00525384/en/}}, number = {RR-7412} }