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, Azadeh will introduce a fresh perspective on using commutativity in program proofs. she 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.

Azadeh 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, she 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. She will also conclude with an overview of several open problems in this area.

Dates

February 29 ,2024 March 11 ,2024

Abstract submission deadline

March 7 ,2024 March 18 ,2024

Paper submission deadline

April 22 ,2024

Accept/Reject notification

May 12 ,2024

Camera ready copy due

May 27-28 ,2024

Metis Spring school

May 29-31 ,2024

Netys Conference

Proceedings

Revised selected papers will be published as a post-proceedings in Springer's LNCS "Lecture Notes in Computer Science"

Partners & Sponsors