E. Zhuchko, I. Varatalu, M. Veanes, and N. Bjørner. "EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination". PLDI ’26. [PDF][Code]
2025
E. Zhuchko, H. Maarand, M. Veanes, and G. Ebner. "Finiteness of Symbolic Derivatives in Lean". ITP ’25. [PDF][Code]
I. Varatalu, M. Veanes, E. Zhuchko, and J. Ernits. "Regex Decision Procedures in Extended RE#". CAV ’25. [PDF][Code]
M. Veanes, T. Ball, G. Ebner, and E. Zhuchko. "Symbolic Automata: Omega-Regularity Modulo Theories". POPL ’25. [PDF][Code]
2024
E. Zhuchko, M. Veanes, and G. Ebner. "Lean Formalization of Extended Regular Expression Matching with Lookarounds". CPP ’24. [PDF][Code]
2022
D. Firsov, S. Laur, and E. Zhuchko. "Unsatisfiability of Comparison-Based Non-Malleability for Commitments". ICTAC ’22. [PDF][Code]