Automated Verification of Fundamental Algebraic Laws - PLDI 2024

Explore a 19-minute video presentation from the PLDI 2024 conference on automated verification of fundamental algebraic laws. Delve into the importance of algebraic properties like commutativity, associativity, and idempotence in computational thinking and software systems. Learn about the Propel verifier, a specialized tool designed to ensure adherence to these properties in application code. Discover how this verifier outperforms state-of-the-art competitors in automatically deducing algebraic properties across various domains. Gain insights into the implementation and evaluation of Propel, which can conjecture auxiliary properties and reason about both equalities and inequalities of expressions. Access supplementary materials, including an artifact archive and web page, to further understand the research and its implications for compiler optimization, big data processing, machine learning, and distributed algorithms.