Skip to Main content Skip to Navigation
Conference papers

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).
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-00777577
Contributor : Claude Marché <>
Submitted on : Friday, January 18, 2013 - 11:14:40 AM
Last modification on : Thursday, July 8, 2021 - 3:48:12 AM
Long-term archiving on: : Friday, April 19, 2013 - 3:05:10 AM

File

size.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00777577⟩

Share

Metrics

Record views

333

Files downloads

322