Abstract: In order to support reasoning about concurrent programs in a rely/guarantee style, we have developed a synchronous refinement algebra similar to Milner’s SCCS. The algebra is based on a general refinement algebra, into which are embedded sub-algebras of instantaneous tests and primitive atomic steps. The synchronous parallel operator executes by synchronizing one atomic step at a time.
This talk overviews the algebra and then focuses on representing fairness. Because we are using synchronous operators it is straightforward to encode fairness assumptions about the interaction of a process with its environment. Hence one can discuss fair execution of a single process, fair termination and fair parallel.
Bio: Ian Hayes is a professor of computing science at the University of Queensland, Brisbane, Australia.
His research interests include program analysis and methods for specifying and reasoning about concurrent and real-time systems based on the rely-guarantee approach and time bands.