Blogs (2) >>
ISMM 2017
Sun 18 Jun 2017 Barcelona, Spain
co-located with PLDI 2017
Sun 18 Jun 2017 16:30 - 17:00 at Aula Master - Session 4: A Deeper Look Chair(s): Steve Blackburn

Existing implementations of dynamic memory allocators (DMA) employ a large spectrum of policies and techniques. The formal specifications of these techniques are quite complicated in isolation and very complex when combined. Therefore, the formal reasoning on a specific DMA implementation is difficult for automatic tools and mostly single-use. This paper proposes a solution to this problem by providing formal models for a full class of DMA, the free list class. To obtain manageable formal reasoning and reusable formal models, we organise these models in a hierarchy ranked by refinement relations. We prove the soundness of models and refinement relations using an off-the-shelf theorem prover. We demonstrate that our hierarchy is a basis for an algorithm theory for the class of free list DMA: it abstracts various existing implementations of DMA and leads to new DMA implementations. We illustrate its application to model-based code generation, testing, run-time verification, and static analysis.

Sun 18 Jun
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30: ISMM 2017 - Session 4: A Deeper Look at Aula Master
Chair(s): Steve BlackburnAustralian National University
ismm-2017-papers16:00 - 16:30
Vini KanvarIndian Institute of Technology (IIT) Bombay, Uday P. Khedker
ismm-2017-papers16:30 - 17:00
Bin FangEast China Normal University (China) and University Paris Diderot and CNRS (France), Mihaela SighireanuIRIF, University Paris Diderot and CNRS, France
ismm-2017-papers17:00 - 17:30
Minjia ZhangMicrosoft Research, Swarnendu BiswasUniversity of Texas at Austin, Michael D. BondOhio State University