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
2 LRI - Laboratoire de Recherche en Informatique
3 PROVAL - Proof of Programs
4 Department of Computing [London]

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).

Domaines: Logique en informatique [cs.LO]

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⟩