I am an Assistant 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 completed my PhD in 2014 at ETH Zurich (Switzerland), under the supervision of Bertrand Meyer. After that, I spent some time as a postdoc at MIT CSAIL, where I worked with Armando Solar-Lezama. I am a 2020 Sloan Fellow and a recipient of the 2020 Intel Rising Stars Award and the 2020 NSF CAREER Award. My research interests are in program synthesis, program verification, and type systems.

I'm looking for graduate students! If you are passionate about program synthesis, types, functional programming, and/or automated reasoning, consider applying to our PhD program (the deadline is Dec 16). All you need to know about grad school is conveniently summarized in this music video featuring our own Ranjit Jhala!

PROJECTS

active projects:

• Hoogle+: type-driven component-based synthesis for Haskell [demo] [pdf] [source]
• SuSLik: synthesis of heap-manipulating programs with separation logic [demo] [pdf] [source]
• Synquid: program synthesis from refinement types [demo] [source] [pdf]
• ReSyn: Synquid + resource types [demo] [pdf] [source]
• Lifty: enforcing information flow security using types and synthesis [pdf] [readme]

older projects:

• 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:

• Hila Peleg (postdoc)
• Zheng (Aaron) Guo
• Rose Kunkel (co-advised with Ranjit Jhala)
• Shraddha Barke
• Michael James
• Tristan Knoth

alumni:

• John Sarracino (PhD, now postdoc at Cornell)
• David Justo (master's thesis)
• Sourav Anand (master's thesis)

PAPERS

• 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

fall 2020	CSE 130: Programming Languages
spring 2020	CSE 130: Programming Languages
winter 2020	CSE 291: Program Synthesis
fall 2019	CSE 130: Programming Languages
winter 2019	CSE 130: Programming Languages
fall 2018	CSE 291: Program Synthesis
spring 2018	CSE 130: Programming Languages
fall 2017	CSE 291: Program Synthesis

ACTIVITIES

recent talks:

2020	Liquid Resource Types for Verification and Synthesis (Chalmers Seminar on Functional Programming) [slides] [video] [example: compress] [example: linear-time compress] [example: insertion sort] [example: insertion sort (fine-grained bound)]
	SuSLik: Synthesis of Safe Pointer-Manipulating Programs (Invited talk at ADSL'20) [slides]
	Synthesizing Programs from Types (Tutorial at POPL'20) [slides]
2019	SuSLik: Synthesis of Safe Pointer-Manipulating Programs (Tutorial at FMCAD'19) [slides]
	Generating Programs from Types (Harvey Mudd College) [slides]
	Type-Driven Program Synthesis (Facebook Menlo Park and Google Brain) [slides]
	Synthesis of Safe Pointer-Manipulating Programs (Purdue and University of Wisconsin) [slides]
2018	Constraint Solvers for the Working PL Researcher (PLMW@ICFP) [slides] [video] [code] [code] [code]
	Type-Driven Program Synthesis (Strangeloop) [slides] [video]

program (co-)chair:

2020	VSTTE
2017	iFM

program committees:

2021	POPL, OOPSLA
2020	ICFP, VMCAI, ADSL
2019	PLDI, SecDev, HCVS, Haskell
2018	OOPSLA, SYNT, POPL
2017	CAV, SYNT
2016	APLAS, FTfJP, SYNT, VSTTE, TAP, iFM, FESCA, VMCAI
2015	PSI, FTfJP, FESCA
2014	RV, FESCA.

external review committees:

2019	ICFP
2018	PLDI