Skip to Main content Skip to Navigation
Conference papers

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

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
Contributor : Claude Marché <>
Submitted on : Wednesday, May 22, 2013 - 10:36:09 PM
Last modification on : Wednesday, September 16, 2020 - 5:20:40 PM
Long-term archiving on: : Friday, August 23, 2013 - 4:17:12 AM


Files produced by the author(s)




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⟩



Record views


Files downloads