Cheney’s copying garbage collector is regarded as a challenging test case for formal approaches to the verification of imperative programs with pointers. The algorithm works for possibly cyclic data structures with unrestricted sharing which cannot be handled by standard separation logics. In addition, the algorithm relocates data and requires establishing an isomorphism between the initial and the final data structure of a program run. We present an implementation of Cheney’s garbage collector in the graph programming language GP 2 and a proof that it is totally correct. Our proof is shorter and less complicated than comparable proofs in the literature. This is partly due to the fact that the GP 2 program abstracts from details of memory management such as address arithmetic. We use sound proof rules previously employed in the verification of GP 2 programs but treat assertions semantically because current assertion languages for graph transformation cannot express the existence of an isomorphism between initial and final graphs.
CITATION STYLE
Wulandari, G. S., & Plump, D. (2018). Verifying a copying garbage collector in GP 2. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11176 LNCS, pp. 479–494). Springer Verlag. https://doi.org/10.1007/978-3-030-04771-9_34
Mendeley helps you to discover research relevant for your work.