Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Automated Verification of Fundamental Algebraic Laws #226

Closed
wants to merge 1 commit into from

Conversation

github-actions[bot]
Copy link
Contributor

@github-actions github-actions bot commented Jan 9, 2025

This paper was randomly selected as your next reading.

Automated Verification of Fundamental Algebraic Laws

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 builtin 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 stateoftheart verifiers on a

Zakhour, George, et al. “Automated Verification of Fundamental Algebraic Laws. Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, June 2024, pp. 76689. Crossref, https://doi.org/10.1145/3656408.

Merge this PR to apply selection.

@github-actions github-actions bot added next-paper paper-vote next paper vote option labels Jan 9, 2025
@nkrusch nkrusch closed this Jan 9, 2025
@nkrusch nkrusch deleted the paper-vote-4 branch January 11, 2025 20:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
next-paper paper-vote next paper vote option
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant