nadia polikarpova

Associate Professor
Department of Computer Science and Engineering
University of California, San Diego
Office: CSE 3102
Email: npolikarpova@ucsd.edu

cv | google scholar | github | twitter

I am an Associate Professor in the Computer Science and Engineering Department at the University of California, San Diego. I am a member of the Programming Systems group. I am also affiliated with the Hannah Arendt Research Center (HARC).

My current research interests are in usable AI-assisted programming (and human-AI collaboration more broadly), civic technology (AI and security for civil society), and computational social science. In the past, I worked on program synthesis, automated verification, and programming languages.

I am the Vice Chair for Graduate Education (aka GradCom Chair) in the CSE department. If you are a current CSE PhD student, feel free to email me or schedule an appointment to discuss any issues related to the PhD program or your experience in the department.

PROJECTS

active and recent:

• HiLDe: exposing AI decisions to programmers [VL/HCC'25]
• GPTScientist: a simple Python library for analyzing tabular data using LLMs [code]
• Solidarity under Repression: a comprehensive study of Russian civil society in 2024 (with HARC) [report] [press coverage]

older projects:

• LEAP: validating AI-generated code with live programming [CHI'24] [code]
• Snippy: live programming by example in Python [UIST'20] [OOPSLA'21] [video] [demo] [code]
• Hoogle+: type-driven component-based synthesis for Haskell [POPL'20] [OOPSLA'20] [demo] [source]
• SuSLik: synthesis of heap-manipulating programs with separation logic [POPL'19] [PLDI'21] [CAV'21] [ICFP'21] [demo] [source]
• Lifty/STORM: information flow control with refinement types [ICFP'20] [OSDI'21] [demo]
• ReSyn: Synquid + resource types [PLDI'19] [ICFP'20] [demo] [source]
• Synquid: program synthesis from refinement types [PLDI'16] [demo] [source]
• AutoProof: an automated deductive verifier for programs that manipulate complex object structures [readme] [demo]
• EiffelBase2: a fully verified container library [source] [pdf]
• Boogaloo: a symbolic execution engine for Boogie [demo] [source]
• CITADEL: dynamic invariant inference meets Design-by-Contract [readme]

TEAM

current:

• Bimal Raj Gyawali
• Raven Rothkopf
• Emmanuel Anaya González
• Eric Mugnier (co-advisor)
• Timothy Zhou (co-advisor)
• Saketh Kasibatla (intermittent co-advisor)
• Cole Kurashige (intermittent co-advisor)

alumni:

• Shraddha Barke (PhD 2024, then Microsoft Research)
• Zheng (Aaron) Guo (PhD 2024, then postdoc at UMich)
• Kasra Ferdowsi (PhD 2024, then cubist)
• Michael James (PhD 2024, then SailPlane)
• Rose Kunkel
• Tristan Knoth (PhD 2023, then jitx)
• Hila Peleg (postdoc, then faculty at Technion)
• John Sarracino (PhD 2021, then postdoc at Cornell)
• David Justo (MS 2020)
• Sourav Anand (MS 2019)

PAPERS

• HiLDe: Intentional Code Generation via Human-in-the-Loop Decoding, Emmanuel Anaya Gonzalez, Raven Rothkopf, Sorin Lerner, Nadia Polikarpova. VL/HCC'25. [arxiv]
• Laurel: Unblocking Automated Verification with Large Language Models Eric Mugnier, Emmanuel Anaya Gonzalez, Nadia Polikarpova, Ranjit Jhala, Zhou Yuanyuan OOPSLA'25 [arxiv]
• HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis Shraddha Barke, Emmanuel Anaya Gonzalez, Saketh Ram Kasibatla, Taylor Berg-Kirkpatrick, Nadia Polikarpova. NeurIPS'24. [arxiv]
• Grammar-Aligned Decoding Kanghee Park, Jiayu Wang, Taylor Berg-Kirkpatrick, Nadia Polikarpova, Loris D'Antoni. NeurIPS'24. [arxiv]
• CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs, Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, Nadia Polikarpova. ICFP'24. [pdf]
• Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis, Ruyi Ji, Yuwei Zhao, Nadia Polikarpova, Yingfei Xiong, Zhenjiang Hu. PLDI'24. [extended]
• Validating AI-Generated Code with Live Programming, Kasra Ferdowsifard, Ruanqianqian Huang, Michael B. James, Nadia Polikarpova, Sorin Lerner. CHI'24. [arxiv]
• Solving Data-centric Tasks using Large Language Models, Shraddha Barke, Christian Poelitz, Carina Suzana Negreanu, Benjamin Zorn, José Cambronero, Andrew D. Gordon, Vu Le, Elnaz Nouri, Nadia Polikarpova, Advait Sarkar, Brian Slininger, Neil Toronto, Jack Williams. NAACL'24 Findings. [arxiv]
• ColDeco: An End User Spreadsheet Inspection Tool for AI-Generated Code, Kasra Ferdowsi, Jack Williams, Ian Drosos, Andrew D. Gordon, Carina Negreanu, Nadia Polikarpova, Advait Sarkar, Benjamin Zorn. VL/HCC'23. [pdf]
• Leveraging Rust Types for Program Synthesis, Jonáš Fiala, Shachar Itzhaky, Peter Müller, Nadia Polikarpova, Ilya Sergey. PLDI'23. Distinguished artifact award [pdf]
• Grounded Copilot: How Programmers Interact with Code-Generating Models, Shraddha Barke, Michael B. James, Nadia Polikarpova. OOPSLA'23. Distinguished paper award [pdf] [preprint]
• babble: Learning Better Abstractions with E-Graphs and Anti-Unification, David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, Nadia Polikarpova. POPL'23. [pdf] [extended]
• Searching Entangled Program Spaces, James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, Nadia Polikarpova. ICFP'22. [pdf] [extended]
• Type-Directed Program Synthesis for RESTful APIs, Zheng Guo, David Cao, Davin Tjong, Jean Yang, Cole Schlesinger, Nadia Polikarpova. PLDI'22. [pdf] [extended]
• LooPy: Interactive Program Synthesis with Control Structures, Kasra Ferdowsifard, Shraddha Barke, Hila Peleg, Sorin Lerner, Nadia Polikarpova. OOPSLA'21. [pdf]
• Certifying the Synthesis of Heap-Manipulating Programs, Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, Ilya Sergey. ICFP'21. [pdf]
• Synthesis of Web Layouts from Examples, Dylan Lukes, John Sarracino, Cora Coleman, Hila Peleg, Sorin Lerner, Nadia Polikarpova. ESEC/FSE'21. [pdf]
• Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities (Invited Paper), Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben Rowe, Ilya Sergey. CAV'21. [pdf]
• STORM: Refinement Types for Secure Web Applications, Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala. OSDI'21. [pdf]
• Cyclic Program Synthesis, Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben Rowe, Ilya Sergey. PLDI'21. Distinguished paper award [pdf] [extended]
• Just-in-Time Learning for Bottom-Up Enumerative Synthesis, Shraddha Barke, Hila Peleg, Nadia Polikarpova. OOPSLA'20. [pdf]
• Digging for Fold: Synthesis-Aided API Discovery for Haskell, Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, Nadia Polikarpova. OOPSLA'20. [pdf]
• Small-Step Live Programming by Example, Kasra Ferdowsifard, Allen Ordookhanians, Hila Peleg, Sorin Lerner, Nadia Polikarpova. UIST'20. [pdf] [video]
• Liquid Information Flow Control, Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama. ICFP'20. Distinguished paper award [pdf] [extended]
• Liquid Resource Types, Tristan Knoth, Adam Reynolds, Di Wang, Nadia Polikarpova, Jan Hoffman. ICFP'20. [pdf] [extended]
• Perfect is the Enemy of Good: Best-Effort Program Synthesis, Hila Peleg, Nadia Polikarpova. ECOOP'20. [pdf]
• Concise Read-Only Specifications for Better Synthesis of Programs with Pointers, Andreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey. ESOP'20. [pdf] [extended]
• Program Synthesis by Type-Guided Abstraction Refinement, Zheng Guo, Michael B. James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, Nadia Polikarpova. POPL'20. [pdf] [extended]
• Constraint-based Learning of Phonological Processes, Shraddha Barke, Rose Kunkel, Nadia Polikarpova, Eric Meinhardt, Eric Bakovic, Leon Bergen. EMNLP'19. [pdf]
• Resource-Guided Program Synthesis, Tristan Knoth, Di Wang, Nadia Polikarpova, Jan Hoffman. PLDI'19. [pdf] [extended]
• Structuring the Synthesis of Heap-Manipulating Programs, Nadia Polikarpova, Ilya Sergey, POPL'19. Distinguished paper award [pdf]
• Automatic Synchronization for GPU Kernels, Sourav Anand, Nadia Polikarpova. FMCAD'18. [pdf]
• Synthesis of Recursive ADT Transformations, Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin S. Lerner, Armando Solar-Lezama. TACAS'17. [pdf]
• Program Synthesis from Polymorphic Refinement Types, Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama. PLDI'16. [pdf] [extended] [slides]
• A Fully Verified Container Library, Nadia Polikarpova, Julian Tschannen, Carlo A. Furia. FM'15. Best paper award [pdf] Extended version in FAoC [pdf]
• AutoProof: Auto-active Functional Verification of Object-oriented Programs (Tool Paper), Julian Tschannen, Carlo A. Furia, Martin Nordio, Nadia Polikarpova. TACAS'15. [pdf]
  Extended version in STTT [pdf]
• Specified and Verified Reusable Components, Nadia Polikarpova. PhD Thesis. [pdf]
• Flexible Invariants Through Semantic Collaboration, Nadia Polikarpova, Julian Tschannen, Carlo A. Furia, Bertrand Meyer. FM'14. [pdf] [supplementary material]
• To Run What No One Has Run Before: Executing an Intermediate Verification Language, Nadia Polikarpova, Carlo A. Furia, Scott West. RV'13. [pdf] [supplementary material]
• What Good Are Strong Specifications? Nadia Polikarpova, Carlo A. Furia, Yu Pei, Yi Wei, Bertrand Meyer. ICSE'13. [pdf] [video] [supplementary material]
• Verified Calculations, K. Rustan M. Leino, Nadia Polikarpova. VSTTE'13. [pdf] [supplementary material]
• Verifying implementations of security protocols by refinement, Nadia Polikarpova, Michał Moskal. VSTTE'12. [pdf]
• The 1st Verified Software Competition: Experience Report, Vladimir Klebanov et. al. FM'11. Best paper award [pdf]
• Specifying Reusable Components, Nadia Polikarpova, Carlo A. Furia, Bertrand Meyer. VSTTE'10. [pdf]
• A comparative study of programmer-written and automatically inferred contracts, Nadia Polikarpova, Ilinca Ciupa, Bertrand Meyer. ISSTA'09. [pdf]

TEACHING

ACTIVITIES

recent talks:

program (co-)chair:

program committees: