Automatic safety proofs for asynchronous memory operations

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. Categories and Subject Descriptors F.3.1 [Logics and Meanings