Techniques For Formal Modellingand Verification On Dynamicmemory Allocators

This thesis contributes to the formal specification and verification of Sequential Dynamic Memory Allocators(SDMA,for short),which are key components of operating systems or standard libraries.SDMA manage the heap part of the data segment of processes.Their implementations employ both complex data structures and low-level operations manipulating the memory.This thesis focuses on SDMA using list data structures to manage the heap chunks available for allocation,i.e.,also called free-list SDMA.The first part of the thesis demonstrates how to obtain formal specifications of free-list SDMA using a refinement-based approach.The thesis defines a hierarchy of models ranked by the refinement relation that capture a large variety of techniques and policies employed by real-work SDMA.This hierarchy forms an algorithm theory for the free-list SDMA and could be extended with other policies.The formal specifications are written in Event-B and the refinements have been proved using the Rodin platform.The thesis investigates applications of the formal specifications obtained,such as model-based testing,code generation and verification.The second part of the thesis defines a technique for inferring precise invariants of existing implementations of SDMA based abstract interpretation.For this,the thesis defines an abstract domain representing sets of states of the SDMA.The abstract domain is based on a fragment of Separation Logic,called SLMA.This fragment captures properties related with the shape and the content of data structures used by the SDMA to manage the heap.The abstract domain is defined as a specific product of an abstract domain for heap shapes with an abstract domain for finite arrays of locations.To obtain compact elements of this abstract domain,the thesis proposes an hierarchical organisation of the abstract values: a first level abstracts the list of all chunks while a second level selects only the chunks available for allocation.The thesis defines transformers of the abstract values that soundly capture the semantics of statements used in SDMA implementations.A prototype implementation of this abstract domain has been used to analyse simple implementations of SDMA.