%0 Book Section %1 pavlovic2010formal %A Pavlovic, Dusko %A Pepper, Peter %A Smith, DouglasR. %B Mathematics of Program Construction %D 2010 %E Bolduc, Claude %E Desharnais, Jules %E Ktari, Béchir %I Springer Berlin Heidelberg %K code collector garbage generation %P 353-376 %R 10.1007/978-3-642-13321-3_20 %T Formal Derivation of Concurrent Garbage Collectors %U http://dx.doi.org/10.1007/978-3-642-13321-3_20 %V 6120 %X 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. %@ 978-3-642-13320-6

@incollection{pavlovic2010formal, abstract = {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.}, added-at = {2014-10-17T19:13:21.000+0200}, author = {Pavlovic, Dusko and Pepper, Peter and Smith, DouglasR.}, biburl = {https://www.bibsonomy.org/bibtex/2b56c4cd0ac7f4afae4aa00c254568cd6/jil}, booktitle = {Mathematics of Program Construction}, description = {Formal Derivation of Concurrent Garbage Collectors - Springer}, doi = {10.1007/978-3-642-13321-3_20}, editor = {Bolduc, Claude and Desharnais, Jules and Ktari, Béchir}, interhash = {adc6ef8881d9279c31969e22e5926934}, intrahash = {b56c4cd0ac7f4afae4aa00c254568cd6}, isbn = {978-3-642-13320-6}, keywords = {code collector garbage generation}, language = {English}, pages = {353-376}, publisher = {Springer Berlin Heidelberg}, series = {Lecture Notes in Computer Science}, timestamp = {2014-10-17T19:13:21.000+0200}, title = {Formal Derivation of Concurrent Garbage Collectors}, url = {http://dx.doi.org/10.1007/978-3-642-13321-3_20}, volume = 6120, year = 2010 }