Sciweavers

Share
IFM
2010
Springer

Certified Absence of Dangling Pointers in a Language with Explicit Deallocation

8 years 4 months ago
Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
Safe is a first-order eager functional language with facilities for programmer controlled destruction and copying of data structures. It provides also regions, i.e. disjoint parts of the heap, where the program allocates data structures. A region is a collection of cells, each one is big enough to allocate a data constructor. The runtime system does not need a garbage collector and all allocation/deallocation actions are done in constant time. Deallocating cells or regions may create dangling pointers. The language is aimed at inferring and certifying memory safety properties in a Proof Carrying Code 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. In this paper we present how to generate formal certificates of the absence of dangling pointers property inferred by the compiler. The certificates are Isabelle/H...
Javier de Dios, Manuel Montenegro, Ricardo Pe&ntil
Added 13 Feb 2011
Updated 13 Feb 2011
Type Journal
Year 2010
Where IFM
Authors Javier de Dios, Manuel Montenegro, Ricardo Peña
Comments (0)
books