Polishing a Rough Diamond: an Enhanced Separation Logic for Heap Space Under Garbage Collection

Title:Polishing a Rough Diamond: an Enhanced Separation Logic for Heap Space Under Garbage Collection

Authors:Alexandre Moine, Arthur Charguéraud and François Pottier

Conference:ASL 2022

Tags:Garbage Collection, Program Verification and Separation Logic

Abstract:

We present a program logic for reasoning about heap space in a λ-calculus equipped with garbage collection and mutable state. Compared with prior work by Madiot and Pottier, we target a higher-level language. This requires us to introduce an assertion to reason about the roots held by the evaluation context.

Polishing a Rough Diamond: an Enhanced Separation Logic for Heap Space Under Garbage Collection

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

1of48

1

2

3

4