POPL 2022 (series) / POPL Research Papers / A Separation Logic for Heap Space under Garbage Collection
A Separation Logic for Heap Space under Garbage CollectionRemote
We present SL♢, a Separation Logic that allows controlling the heap space consumption of a program in the presence of dynamic memory allocation and garbage collection. A user of the logic works with space credits, a resource that is consumed when an object is allocated and produced when a group of objects is logically deallocated, that is, when the user is able to prove that it has become unreachable and therefore can be collected. To prove such a fact, the user maintains pointed-by assertions that record the immediate predecessors of every object. Our calculus, SpaceLang, has mutable state, shared-memory concurrency, and code pointers. We prove that SL♢ is sound and present several simple examples of its use.
Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change
Wed 19 Jan
Displayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 25mTalk | A Separation Logic for Heap Space under Garbage CollectionRemote POPL DOI Media Attached | ||
10:45 25mResearch paper | Simuliris: A Separation Logic Framework for Verifying Concurrent Program OptimizationsDistinguished PaperRemote POPL Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Ralf Jung MPI-SWS, Hoang-Hai Dang MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS DOI Media Attached | ||
11:10 25mResearch paper | Concurrent Incorrectness Separation LogicRemote POPL Azalea Raad Imperial College London, Josh Berdine Meta, Derek Dreyer MPI-SWS, Peter W. O'Hearn Meta; University College London DOI Media Attached | ||
11:35 25mResearch paper | On Incorrectness Logic and Kleene Algebra with Top and TestsInPerson POPL Cheng Zhang Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University DOI Media Attached |