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...

• Type: Journal
• Year: 2010
• Where: IFM
• Authors: Javier de Dios, Manuel Montenegro, Ricardo Peña
• Keywords: Data Structures, Eager Functional Language, Formal Methods, IFM 2010, Programmer Controlled Destruction