body
Publications
Peer-reviewed international journals
- Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology (Extended Version). [preprint]
Y. Zakowski, D. Cachera, D. Demange, G. Petri, D. Pichardie, S. Jagannathan, J. Vitek. JAR 2018.
Peer-reviewed international conferences
- Semantic Reasoning about the Sea of Nodes. [preprint]
D. Demange, Y. Fernández de Retana, and D. Pichardie. CC 2018. - Verified Compilation of Linearizable Data Structures. [preprint]
Y. Zakowski, D. Cachera, D. Demange and D. Pichardie. SAC 2018, SVT. - Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology. [preprint]
Y. Zakowski, D. Cachera, D. Demange, G. Petri, D. Pichardie, S. Jagannathan, J. Vitek. ITP 2017. - Mechanizing Conventional SSA for a Verified Destruction with Coalescing. [preprint]
D. Demange, Y. Fernández de Retana. CC 2016. - Verifying Fast and Sparse SSA-based Optimizations in Coq. [preprint]
D. Demange, D. Pichardie and L. Stefanesco. CC 2015. - Validating Dominator Trees for a Fast, Verified Dominance Test. [preprint]
S. Blazy, D. Demange and D. Pichardie. ITP 2015.
Peer-reviewed international workshops
- An Extended Buffered Memory Model With Full Reorderings. [preprint]
G. Cabon, D. Cachera, and D. Pichardie. FTfJP 2016.
Theses
- Vers la compilation vérifiée de Sea of Nodes : propriétés et raisonnement sémantiques. [HAL]
Yon Fernández de Retana. Manuscrit de thèse. Université Rennes 1. 2018.