Automated Verification of Fundamental Algebraic Laws
Journal
Proceedings of the ACM on Programming Languages
ISSN
2475-1421
Type
journal article
Date Issued
2024-06
Author(s)
Abstract
Algebraic laws of functions in mathematics-such as commutativity, associativity, and idempotence-are often used as the basis to derive more sophisticated properties of complex mathematical structures and are heavily used in abstract computational thinking. Algebraic laws of functions in coding, however, are rarely considered. Yet, they are essential. For example, commutativity and associativity are crucial to ensure correctness of a variety of software systems in numerous domains, such as compiler optimization, big data processing, data flow processing, machine learning or distributed algorithms and data structures. Still, most programming languages lack built-in mechanisms to enforce and verify that operations adhere to such properties. In this paper, we propose a verifier specialized on a set of fundamental algebraic laws that ensures that such laws hold in application code. The verifier can conjecture auxiliary properties and can reason about both equalities and inequalities of expressions, which is crucial to prove a given property when other competitors do not succeed. We implement these ideas in the Propel verifier. Our evaluation against five state-of-the-art verifiers on a total of 142 instances of algebraic properties shows that Propel is able to automatically deduce algebraic properties in different domains that rely on such properties for correctness, even in cases where competitors fail to verify the same properties or time out.
Keywords
Algebraic Properties
Type Systems
Verification
Publisher
ACM
Publisher place
New York, NY, USA
Volume
8
Number
PLDI
Start page
178:1
End page
178:24
Pages
24
Event Location
Copenhagen, Denmark
File(s)![Thumbnail Image]()
Name
2024_Automated-Verification-of-Fundamental-Algebraic-Laws.pdf
Size
358.94 KB
Format
Adobe PDF
Checksum (MD5)
ee52af6ddfea250e470a8f3cd795123c