Certified Absence of Dangling Pointers in a Language with Explicit Deallocation

Abstract : Safe is a first-order eager functional language with facilities for programmer controlled destruction of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program allocates data structures, so that the runtime system does not need a garbage collector. A region is a collection of cells, each one big enough to allocate a data constructor. Deallocating cells or regions may create dangling pointers. The language is aimed at inferring and certifying memory safety properties in a Proof Carrying Code like environment. Some of its analyses have been presented elsewhere. The one relevant to this paper is a type system and a type inference algorithm guaranteeing that well-typed programs will be free of dangling pointers at runtime. Here we present how to generate formal certificates about the absence of dangling pointers property inferred by the compiler. The certificates are Isabelle/HOL proof scripts which can be proof-checked by this tool when loaded with a database of previously proved theorems. The key idea is proving an Isabelle/HOL theorem for each syntactic construction of the language, relating the static types inferred by the compiler to the dynamic properties about the heap that will be satisfied at runtime.
Type de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.305-319, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00524597
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : vendredi 8 octobre 2010 - 11:53:26
Dernière modification le : mercredi 28 mars 2018 - 14:38:34
Document(s) archivé(s) le : lundi 10 janvier 2011 - 11:42:51

Fichier

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

Identifiants

  • HAL Id : inria-00524597, version 1

Collections

Citation

Javier De Dios, Manuel Montenegro, Ricardo Peña. Certified Absence of Dangling Pointers in a Language with Explicit Deallocation. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.305-319, 2010, Lecture Notes in Computer Science. 〈inria-00524597〉

Partager

Métriques

Consultations de la notice

80

Téléchargements de fichiers

81