Compositional Invariant Checking for Overlaid and Nested Linked Lists

Abstract : We introduce a fragment of separation logic, called NOLL, for auto- mated reasoning about programs manipulating overlaid and nested linked lists, where overlaid means that the lists may share the same set of objects. The dis- tinguishing features of NOLL are: (1) it is parametrized by a set of user-defined predicates specifying nested linked list segments, (2) a "per-field" version of the separating conjunction allowing to share locations but not fields, and (3) it can express sharing constraints between list segments. We prove that checking the entailment between two NOLL formulas is co-NP complete. For this result, the decision procedure for entailment is based on a small model property. We also provide an effective procedure for checking entailment in NOLL, which first con- structs a Boolean abstraction of the two formulas, in order to infer all the implicit constraints, and then, it checks the existence of a homomorphism between the two formulas, viewed as graphs. We have implemented this procedure and ap- plied it on verification conditions generated from several interesting case studies that manipulate overlaid and nested data structures.
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00768389
Contributeur : Mihaela Sighireanu <>
Soumis le : vendredi 21 décembre 2012 - 13:31:19
Dernière modification le : jeudi 11 janvier 2018 - 06:17:42
Document(s) archivé(s) le : dimanche 18 décembre 2016 - 07:55:06

Fichier

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

Identifiants

  • HAL Id : hal-00768389, version 1

Collections

Citation

Constantin Enea, Vlad Saveluc, Mihaela Sighireanu. Compositional Invariant Checking for Overlaid and Nested Linked Lists. [Research Report] 2012, pp.27. 〈hal-00768389〉

Partager

Métriques

Consultations de la notice

121

Téléchargements de fichiers

226