Automatic safety proofs for asynchronous memory operations

Published in Principles and practice of parallel programming (PPoPP), 2011

Abstract: We present a work-in-progress proof system and tool, based on separation logic, for analysing memory safety of multicore programs that use asynchronous memory operations.