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]

E. Zhuchko, M. Veanes, and G. Ebner.
"Lean Formalization of Extended Regular Expression Matching with Lookarounds". CPP ’24.
[PDF] [Code]

D. Firsov, S. Laur, and E. Zhuchko.
"Unsatisfiability of Comparison-Based Non-Malleability for Commitments". ICTAC ’22.
[PDF] [Code]