Embedding Rely-Guarantee Reasoning in Temporal Logic

The combination of temporal logic and rely-guarantee reasoning is a solid approach for the verification of concurrent programs. We describe a formalization of rely-guarantee reasoning within the temporal logic framework of the interactive prover KIV. Our previous encoding has been enhanced to permit simpler rely conditions and enriched to make it more expressive. Moreover, an instance of the new theory is defined to better exploit the symmetry inherent in many concurrent systems, by considering a single pair of processes only. We verify the resulting local proof obligations, applying symbolic execution to show memory safety, linearizability and lock-freedom of a shared stack that recycles memory.