Paper Info
Title
Verifying the Safety of a Practical Concurrent Garbage Collector
Abstract
We describe our experience in the mechanical verification of the safety invariants of an asynchronous garbage-collection algorithm [1], using the TLP system [2]. We only give a cursory overview of the algorithm and its formalisation. Our main focus is on the lessons learned from carrying a sizeable (22,000+ lines) formal proof through an off-the-shelf prover. In particular, we found the TLP style of structured proofs to be particularly effective for organising, writing, and managing proof scripts.
Year
DOI
Venue
1996
10.1007/3-540-61474-5_103
CAV
Keywords
Field
DocType
concurrent garbage collector,garbage collection,garbage collector
Asynchronous communication,Computer science,Theoretical computer science,Mathematical proof,Garbage collection,Invariant (mathematics),Gas meter prover,Scripting language,Formal proof
Conference
ISBN
Citations 
PageRank 
3-540-61474-5
16
0.98
References 
Authors
5
1
Name
Order
Citations
PageRank
Georges Gonthier12275195.06