Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Verified Concurrent Programmes: Laws of Programming with Concurrency

Speaker  Tony Hoare

Affiliation  MSR Cambridge

Host  Tony Hoare

Duration  01:06:46

Date recorded  13 June 2013

The talk starts with a summary of the familiar algebraic properties of choice in a program and of both sequential and concurrent composition. These properties validate the proof rules of Hoare logic (augmented by concurrency), as well as the transition rules of a process algebra (augmented by sequential composition). The laws are then proved true of a simple causal model of the behaviour of programs when executed. The model is generic, and can be particularised to different programming languages, and different notions of correctness. This theoretical result gives hope that any Software Engineering tool that is based on the laws can safely interwork with any other such tool.

©2013 Microsoft Corporation. All rights reserved.
> Verified Concurrent Programmes: Laws of Programming with Concurrency