This thesis explores the use of ownership as a key auxiliary variable within the Owicki-Gries framework to aid in verification of concurrent programs. Ownership has been prominently used within the field as a means to isolate parts of the shared memory prone to interference, for example in Separation Logic. However, we make systematic use of the auxiliary variable to verify interference freedom as described by the Owicki-Gries framework without notational overheads associated with the more fine-grained approaches. We identify shared, by the involved processes, variables and establish, whether safe transfer of access rights to the shared memory can be violated. Following a discussion on the strength of this approach in the context of smaller examples, we formalise our method and demonstrate its elegance in verification of safety of the Peterson's Algorithm.

In this work we include verification of a ring buffer, developed by Amazon, under restriction of sequential consistency (SC). The partial library only provides methods for reserving (acquiring) and releasing addresses within the buffer, obliging the client to implement additional functionality (including an additional shared queue) to enable full synchronisation between a writer and a reader. We verify correctness of the Amazon ring buffer (ARB) and show that the ARB satisfies both safety and progress.

Subsequent work includes another paper presenting a verification of safety of the Read-Copy Update (RCU) lock-free synchronisation mechanism that is used extensively in the Linux kernel. We develop and verify an RCU implementation under RC11 (a restricted version of C11 weak memory model, which includes relaxed and release-acquire accesses), increasing the verification challenge. In our proof, we extend a recent Owicki-Gries logic for RC11, which we combine with our ownership model to show correctness.

All our proofs have been mechanised in the Isabelle/HOL theorem prover.