Separation Predicates: a Taste of Separation Logic in First-Order Logic

François Bobot 1, 2 Jean-Christophe Filliâtre 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program veri cation using a traditional rst-order logic. The purpose is to bene t from existing speci cation languages, veri cation condition generators, and automated theorem provers. Separation predicates are automatically derived from user-de ned inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is speci- ed in C/ACSL and veri ed in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3.
Document type :
Conference papers
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-00825088
Contributor : Claude Marché <>
Submitted on : Wednesday, May 22, 2013 - 10:36:09 PM
Last modification on : Monday, September 3, 2018 - 12:40:01 PM
Long-term archiving on : Friday, August 23, 2013 - 4:17:12 AM

File

bobot12icfem.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

François Bobot, Jean-Christophe Filliâtre. Separation Predicates: a Taste of Separation Logic in First-Order Logic. 14th International Conference on Formal Ingineering Methods (ICFEM), Nov 2012, Kyoto, Japan. pp.167-181, ⟨10.1007/978-3-642-34281-3_14⟩. ⟨hal-00825088⟩

Share

Metrics

Record views

468

Files downloads

290