There is a rich history of using commutativity in reasoning about programs. Commutativity of atomic program steps has been exploited in dynamic program analyses, for instance, in predictive testing for generic correctness properties like atomicity and data race freedom. On the static side, it has been used as the basis of type-and-effect systems, optimizations in model checking, and construction of program proofs, both automated and human-assisted.

In this talk, I will introduce a fresh perspective on using commutativity in program proofs. I will discuss a line of ongoing work based on the simple and elegant theory of commutativity, introduced by Mazurkiewicz in 1987, that puts commutativity reasoning at the heart of proof search in a broad set of automated verification goals. These include hypersafety verification of sequential and concurrent programs, and safety and liveness verification of concurrent and distributed programs. The emerging thesis is that by taking advantage of commutativity, one may discover a substantially simpler verification task to replace the original in many cases. Consequently, the simpler task may succeed where the original fails, for example due to theoretical or practical shortcomings of available theorem proving support. More specifically, a different program, which is easier to verify, is proven correct in place of the original one and commutativity is used as a way of soundly carrying the verification results back.

I will introduce a language-theoretic framework in which the program, the property, and the commutativity relation can be formalized in a way that an algorithmic search for these simpler verification tasks can be conducted. Furthermore, I will discuss how this framework can be used to tackle other research questions such as using contextual and abstract commutativity, and soundly combining multiple sound commutativity relations. I will conclude with an overview of several open problems in this area.

I am a Professor at University of Toronto.