Elizaveta (Liza) Pertseva

About

Hello! I am a Ph.D. candidate in Computer Science at Stanford University, advised by Professor Clark Barrett . My research develops automated reasoning techniques for emerging verification domains, with recent applications to cryptographic systems and spatial reasoning. I am particularly interested in verification problems that require new formalizations or reasoning across multiple domains (and/or SMT theories), including bitvectors, finite fields, integers and sets.

Previously, I was at the University of California, San Diego , where I worked with Professor Nadia Polikarpova and Professor Taylor Berg-Kirkpatrick on regular-expression synthesis from positive examples. I also worked with Professor Michael Coblenz on Haskell debugging and scientific computing.

Research Interests

My research interests include: SMT solvers, interactive theorem provers, program synthesis, and cryptography.

I currently work in cvc5 and Lean.

Publications

• Elizaveta Pertseva, Valentin Robert, Clark Barrett, and James Parker. Automating Bitvector and Finite Field Equivalence Proofs in Lean. Computer Aided Verification (CAV), 2026. [pdf]
• Pedro Saccomani, Abdalrhman Mohamed, Elizaveta Pertseva, Daniela Kaufmann, Cesare Tinelli, Clark Barrett, and Haniel Barbosa. Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean. Formal Methods in Computer-Aided Design (FMCAD), 2026. To appear.
• Elizaveta Pertseva, Alexander J. Root, Nestan Tsiskaridze, Fredrik Kjolstad, and Clark Barrett. Topological Predicate Synthesis via SyGuS. FMCAD Student Forum, 2026. To appear.
• Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Işıl Dillig, and Clark Barrett. Integer Reasoning Modulo Different Constants in SMT. 37th International Conference on Computer Aided Verification (CAV), 2025. [pdf]
• Elizaveta Pertseva, Melinda Chang, Ulia Zaman, and Michael Coblenz. A Theory of Scientific Programming Efficacy. 46th International Conference on Software Engineering (ICSE), 2024. [pdf]
• Silei Xu, Shicheng Liu, Theo Culhane, Elizaveta Pertseva, Meng-Hsi Wu, Sina J. Semnani, and Monica S. Lam. Fine-tuned LLMs Know More, Hallucinate Less with Few-Shot Sequence-to-Sequence Semantic Parsing over Wikidata. Conference on Empirical Methods in Natural Language Processing (EMNLP), 2023. [pdf]
• Ruanqianqian (Lisa) Huang, Elizaveta Pertseva, Michael Coblenz, and Sorin Lerner. How Do Haskell Programmers Debug? 13th Workshop on the Intersection of HCI and PL (PLATEAU), 2023. [pdf]
• Nikolai Vogler, Kartik Goyal, Kishore P. V. Reddy, Elizaveta Pertseva, Cristopher Warren, Max G’Sell, and Taylor Berg-Kirkpatrick. Contrastive Attention Networks for Attribution of Early Modern Print. 37th Association for the Advancement of Artificial Intelligence Conference (AAAI), 2023. [pdf]
• Elizaveta Pertseva, Mark Barbone, Joey Rudek, and Nadia Polikarpova. Regex+: Synthesizing Regular Expressions from Positive Examples. 11th Workshop on Synthesis (SYNT), 2022. [pdf]

News

• [July 2026] I will present our paper “Automating Bitvector and Finite Field Equivalence Proofs in Lean” at CAV 2026.
• [July 2026] I will be a panelist at the FLoC 2026 Mentoring Workshop .
• [July 2026] Our work “Topological Predicate Synthesis via SyGuS” was accepted to the FMCAD 2026 Student Forum.
• [July 2026] Our paper “Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean” was accepted to FMCAD 2026.
• [March 2026] I led an introductory session on SMT solvers at the HACS workshop.
• [July 2025] I presented our paper “Integer Reasoning Modulo Different Constants in SMT” at CAV 2025.

Teaching and Mentoring

• [Summer 2026] Mentor for Ishani Mukherjee through the Stanford CURIS undergraduate research program, working on cryptographic verification benchmarks for CSLib.
• [Spring 2026] Mentor for Daniel James through the Stanford CURIS undergraduate research program working on the pipeline for CSLib.
• [Fall 2025] Course Assistant for CS 120: Introduction to AI Safety .
• [Spring 2022] Tutor for CSE 130: Programming Languages (Instructor: Nadia Polikarpova ).

Industry Experience

• Research Intern, Galois, Inc. (Summer 2025)
  Verified Zero-Knowledge Proof systems using Lean.
• Software Engineering Intern, Amazon (Summer 2022)

Service

• Panelist, FLoC 2026 Mentoring Workshop (2026)
• Subreviewer, TACAS (2026)
• Subreviewer, IJCAR (2026)
• Co-organizer, Stanford–Berkeley Women in Engineering Research Meetup (2025)
• Subreviewer, TACAS (2025)
• Artifact evaluator, TACAS (2025)
• CAV Volunteer (2025)
• POPL Volunteer (2023)
• FLoC Volunteer (2022)

Contact

📧 pertseva[-at-]stanford[-dot-]edu