Concurrent software is difficult to reason about and impossible to verify by testing. Yet much software written today is concurrent. We therefore need practical mechanisms to automatically verify concurrent software. I propose a way of annotating concurrent programs based on fractional permissions, dynamic frames, and explicit transfer of permissions. An annotated program may be automatically verified by translating to a sequential intermediate verification language such as the Boogie IVL and then verifying a set of sequential fragments.
