A New Perspective on Commutativity in Verification

Explore a fresh perspective on commutativity in program verification through this 58-minute conference talk from POPL'24. Delve into Azadeh Farzan's presentation on leveraging commutativity reasoning to simplify complex verification tasks across sequential, concurrent, and distributed programs. Discover how Mazurkiewicz's 1987 theory of commutativity can be applied to various automated verification goals, including hypersafety, safety, and liveness verification. Learn about a language-theoretic framework that formalizes programs, properties, and commutativity relations, enabling algorithmic searches for simplified verification tasks. Gain insights into the potential of commutativity-based approaches to overcome limitations in current theorem proving techniques. Explore topics such as contextual and abstract commutativity, combining multiple commutativity relations, and open problems in this emerging field of program verification research.