Understanding concurrent programs using rely-guarantee thinking (2013-2015)

Concurrent programs are becoming more pervasive with the wide availability of multi-core processors in standard computers and devices such as smart phones. The research challenge of this project is to devise better methods for deriving and reasoning about concurrent programs in order to effectively utilize these platforms. Concurrent programs are notoriously difficult to debug and test, and in practice often exhibit unpredictable behaviour or deadlock. Our focus is on design techniques for concurrent programs based on rely-guarantee thinking that afford a deeper understanding of their behaviour and hence guide the design of more reliable systems that can exploit the available hardware parallelism to provide enhanced performance.