Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic

Clément Hurlin 1 François Bobot 2, 3 Alexander Summers 4
1 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
3 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : We describe an algorithm to disprove entailment between separation logic formulas. We abstract models of formulas by their size and check whether two formulas have models whose sizes are compatible. Given two formulas A and B that do not have compatible models, we can conclude that A 0 B. We provide two different abstractions (of different precision) of models. Our algorithm is of interest wherever entailment checking is performed (such as in program verifiers).
Type de document :
Communication dans un congrès
International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09), Jul 2009, Genova, Italy. 2009
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00777577
Contributeur : Claude Marché <>
Soumis le : vendredi 18 janvier 2013 - 11:14:40
Dernière modification le : lundi 3 septembre 2018 - 12:40:01
Document(s) archivé(s) le : vendredi 19 avril 2013 - 03:05:10

Fichier

size.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00777577, version 1

Collections

Citation

Clément Hurlin, François Bobot, Alexander Summers. Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic. International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO'09), Jul 2009, Genova, Italy. 2009. 〈hal-00777577〉

Partager

Métriques

Consultations de la notice

266

Téléchargements de fichiers

153