The advent of non-volatile memory (NVM) technologies is expected to transform how software systems are structured fundamentally, making the task of \emph{correct} programming significantly harder. This is because ensuring that memory stores persist in the correct order is challenging, and requires low-level programming to flush the cache at appropriate points. This has in turn resulted in a noticeable \emph{verification gap}. %causing a significant verification burden.
To address this, we study the verification of NVM programs, and present \emph{Persistent Owicki-Gries} (POG), the first program logic for reasoning about such programs. We prove the soundness of POG over the recent Intel-x86 model, which formalises the out-of-order persistence of memory stores and the semantics of the Intel cache line flush instructions. We then use POG to verify several programs that interact with NVM.
