Heap-Dependent Expressions in Separation Logic

Abstract : Separation logic is a popular specification language for imperative programs where the heap can only be mentioned through points-to assertions. However, separation logic's take on assertions does not match well with the classical view of assertions as boolean, side effect-free, potentially heap-dependent expressions from the host programming language familiar to many developers. In this paper, we propose a variant of separation logic where side effect-free expressions from the host programming language, such as pointer dereferences and invocations of pure methods, can be used in assertions. We modify the symbolic execution-based verification algorithm used in Smallfoot to support mechanized checking of our variant of separation logic. We have implemented this algorithm in a tool and used the tool to verify some interesting programming patterns.
Type de document :
Communication dans un congrès
John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.170-185, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_14〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01055155
Contributeur : Hal Ifip <>
Soumis le : lundi 11 août 2014 - 16:31:35
Dernière modification le : vendredi 11 août 2017 - 16:16:36
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 22:15:40

Fichier

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

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Jan Smans, Bart Jacobs, Frank Piessens. Heap-Dependent Expressions in Separation Logic. John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.170-185, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_14〉. 〈hal-01055155〉

Partager

Métriques

Consultations de la notice

244

Téléchargements de fichiers

94