A Simplified Account of Region Inference

Region inference is a program analysis which statically determines regions of memory in which values are stored. Regions are allocated and de-allocated according to a stack discipline. Region inference is an attractive alternative to dynamic memory management via garbage collection for the implementation of mission-critical applications, of inter-operating system components, of certifiable software. In the aim of putting region-based memory management to work for the design and implementation of real-time system software, the goal of the present article is to consolidate present knowledge on region-based memory management by giving a simplified account of region inference. We achieve this goal by giving an inductive proof of correctness for region inference w.r.t. a small step operational semantics and by defining a sound, fixed-point iterative, inference algorithm