A formal soundness proof of region-based memory management for object-oriented paradigm

Florin Craciun, Shengchao Qin, Wei-Ngan Chin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

72 Downloads (Pure)

Abstract

Region-based memory management has been proposed as a viable alternative to garbage collection for real-time applications and embedded software. In our previous work we have developed a region type inference algorithm that provides an automatic compile-time region-based memory management for object-oriented paradigm. In this work we present a formal soundness proof of the region type system that is the target of our region inference. More precisely, we prove that the object-oriented programs accepted by our region type system achieve region-based memory management in a safe way. That means, the regions follow a stack-of-regions discipline and regions deallocation never create dangling references in the store and on the program stack. Our contribution is to provide a simple syntactic proof that is based on induction and follows the standard steps of a type safety proof. In contrast the previous safety proofs provided for other region type systems employ quite elaborate techniques.
Original languageEnglish
Title of host publicationFormal methods and software engineering
PublisherSpringer Verlag
Pages126-146
ISBN (Print)9783540881933
DOIs
Publication statusPublished - 2008
EventInternational Conference on Formal Methods and Software Engineering - Kitakyushu-City, Japan
Duration: 27 Oct 200831 Oct 2008
Conference number: 10

Conference

ConferenceInternational Conference on Formal Methods and Software Engineering
CountryJapan
CityKitakyushu-City
Period27/10/0831/10/08

Bibliographical note

Author can archive post-print (ie final draft post-refereeing).

Fingerprint Dive into the research topics of 'A formal soundness proof of region-based memory management for object-oriented paradigm'. Together they form a unique fingerprint.

  • Cite this

    Craciun, F., Qin, S., & Chin, W-N. (2008). A formal soundness proof of region-based memory management for object-oriented paradigm. In Formal methods and software engineering (pp. 126-146). Springer Verlag. https://doi.org/10.1007/978-3-540-88194-0-10