Sciweavers

19
Voted
MPC
2010
Springer

Formal Derivation of Concurrent Garbage Collectors

13 years 9 months ago
Formal Derivation of Concurrent Garbage Collectors
Concurrent garbage collectors are notoriously difficult to implement correctly. Previous approaches to the issue of producing correct collectors have mainly been based on posit-and-prove verification or on the application of domain-specific templates and transformations. We show how to derive the upper reaches of a family of concurrent garbage collectors by refinement from a formal specification, emphasizing the application of domain-independent design theories and transformations. A key contribution is an extension to the classical lattice-theoretic fixpoint theorems to account for the dynamics of concurrent mutation and collection.
Dusko Pavlovic, Peter Pepper, Douglas R. Smith
Added 20 Jul 2010
Updated 20 Jul 2010
Type Conference
Year 2010
Where MPC
Authors Dusko Pavlovic, Peter Pepper, Douglas R. Smith
Comments (0)