Starting Date: June 2024
Prerequisites: Good knowledge of C++ and automata theory
Will results be assigned to University: No
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.
In this project we will explore extending symbolic extensions of the Parikh’s theorem [1] to automata with registers [2].
[1] Matthew Hague, Artur Jeż, and Anthony W. Lin. 2024. Parikh’s Theorem Made Symbolic. Proc. ACM Program. Lang. 8, POPL, Article 65 (January 2024), 33 pages. https://doi.org/10.1145/3632907
[2] D’Antoni, L., Ferreira, T., Sammartino, M., Silva, A. (2019). Symbolic Register Automata. In: Dillig, I., Tasiran, S. (eds) Computer Aided Verification. CAV 2019. Lecture Notes in Computer Science(), vol 11561. Springer, Cham. https://doi.org/10.1007/978-3-030-25540-4_1