Presenter: Professor Ian Hayes, University of Queensland, Australia
Abstract: To reason compositionally about concurrent programs one needs to be able to reason about a process in the context of the interference from its environment. Cliff Jones introduced an elegant approach to handle reasoning about interference in terms of rely and guarantee conditions, each of which is a binary relation between program states. Here we examine guarantee and rely separately and derive laws for each as well as in combination for handling parallel composition.