Automated Verification of Fundamental Algebraic Laws

data/desc.txt

@@ -1,3 +1,3 @@
-Parikh’s Theorem Made Symbolic
-Hague, Matthew, et al. “Parikh’s Theorem Made Symbolic.” Proceedings of the ACM on Programming Languages, vol. 8, no. POPL, Jan. 2024, pp. 1945–77. Crossref, https://doi.org/10.1145/3632907.
-Parikh’s Theorem is a fundamental result in automata theory with numerous applications in computer science. These include software verification (e.g. infinite-state verification, string constraints, and theory of arrays), verification of cryptographic protocols (e.g. using Horn clauses modulo equational theories) and database querying (e.g. evaluating path-queries in graph databases), among others. Parikh’s Theorem states that the letter-counting abstraction of a language recognized by finite automata or context-free grammars is definable in Linear Integer Arithmetic (a.k.a. Presburger Arithmetic). In fact, there is a linear-time algorithm computing existential Presburger formulas capturing such abstractions, which enables an efficient analysis via SMT-solvers. Unfortunately, real-world applications typically require large alphabets (e.g. Unicode, containing a‍million of characters) — which are well-known to be not amenable to explicit treatment of the alphabets — or even worse infinite alphabets. Symbolic automata have proven in the last decade to be an effective algorithmic framework for handling large finite or even infinite alphabets. A symbolic automaton employs an effective boolean algebra, which offers a symbolic representation of character sets (i.e. in terms of predicates) and often lends itself to an exponentially more succinct representation of a language. Instead of letter-counting, Parikh’s Theorem for symbolic automata amounts to counting the number of times different predicates are satisfied by an input sequence. Unfortunately, naively applying Parikh’s Theorem from classical automata theory to symbolic automata yields existential Presburger formulas of exponential size. In this paper, we provide a new construction for Parikh’s Theorem for symbolic automata and grammars, which avoids this exponential blowup: our algorithm computes an existential formula in polynomial-time over (quantifier-free) Presburger and the base theory. In fact, our algorithm extends to the model of parametric symbolic grammars, which are one of the most expressive models of languages over infinite alphabets. We have implemented our algorithm and show it can be used to solve string constraints that are difficult to solve by existing solvers.
+Automated Verification of Fundamental Algebraic Laws
+Zakhour, George, et al. “Automated Verification of Fundamental Algebraic Laws.” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, June 2024, pp. 766–89. Crossref, https://doi.org/10.1145/3656408.
+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.

data/history.txt

@@ -35,4 +35,5 @@ https://doi.org/10.1145/3607862
 https://doi.org/10.1145/3586038
 https://doi.org/10.1145/3622837
 https://doi.org/10.1145/3622820
-https://doi.org/10.1145/3632907
+https://doi.org/10.1145/3632907
+https://doi.org/10.1145/3656408

data/next.txt

@@ -0,0 +1 @@
+https://doi.org/10.1145/3656408

data/past.txt

@@ -0,0 +1,2 @@
+
+https://doi.org/10.1145/3656408

docs/index.md

@@ -26,7 +26,7 @@ Current [reading group policies](policies).
 | \#  | Date        | Description         |
 |:---:|:------------|:--------------------|
 | 0.  | January 10  | ⚠️ _First meeting is canceled for snow storm_ |
-| 1.  | January 17  | Paper 1 discussion  |
+| 1.  | January 17  | Automated Verification of Fundamental Algebraic Laws  |
 | 2.  | January 24  | Paper 2 discussion  | 
 | 3.  | January 31  | Paper 3 discussion  |
 | 4.  | February 7  | Paper 4 discussion  |

docs/papers.md

@@ -0,0 +1 @@
+1. Zakhour, George, et al. “Automated Verification of Fundamental Algebraic Laws.” Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, June 2024, pp. 766–89. Crossref, <a href='https://doi.org/10.1145/3656408' target='_blank'>https://doi.org/10.1145/3656408</a>.