VSync: push-button verification and optimization for synchronization primitives on weak memory models. - Jonas Oberhauser; Rafael Lourenco de Lima Chehab; Diogo Behrens; Ming Fu; Antonio Paolillo; Lilith Oberhauser; Koustubha Bhat; Yuzhong Wen; Haibo Chen 001; Jaeho Kim; Viktor Vafeiadis (ASPLOS, 2021)

CLoF: A Compositional Lock Framework for Multi-level NUMA Systems. - Rafael Lourenco de Lima Chehab; Antonio Paolillo; Diogo Behrens; Ming Fu; Hermann Härtig; Haibo Chen 001 (SOSP, 2021)

VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report). - Jonas Oberhauser; Rafael Lourenco de Lima Chehab; Diogo Behrens; Ming Fu; Antonio Paolillo; Lilith Oberhauser; Koustubha Bhat; Yuzhong Wen; Haibo Chen 001; Jaeho Kim; Viktor Vafeiadis (CoRR, 2021)

Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models. - Antonio Paolillo; Hernán Ponce de León; Thomas Haas; Diogo Behrens; Rafael Lourenco de Lima Chehab; Ming Fu; Roland Meyer 001 (CoRR, 2021)