Please use this identifier to cite or link to this item:
|Title:||A formal soundness proof of region-based memory management for object-oriented paradigm|
|Citation:||Craciun, F.,Qin, S.,Chin, W.-N. (2008). A formal soundness proof of region-based memory management for object-oriented paradigm. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5256 LNCS : 126-146. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-540-88194-0-10|
|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. © 2008 Springer Berlin Heidelberg.|
|Source Title:||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 22, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.