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.
Type de document :
Communication dans un congrès
14th International Conference on Formal Ingineering Methods (ICFEM), Nov 2012, Kyoto, Japan. Springer, 7635, pp.167-181, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-34281-3_14〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00825088
Contributeur : Claude Marché <>
Soumis le : mercredi 22 mai 2013 - 22:36:09
Dernière modification le : vendredi 10 novembre 2017 - 14:52:02
Document(s) archivé(s) le : vendredi 23 août 2013 - 04:17:12

Fichier

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

Identifiants

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. Springer, 7635, pp.167-181, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-34281-3_14〉. 〈hal-00825088〉

Partager

Métriques

Consultations de la notice

239

Téléchargements de fichiers

179