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 almost three years as a postdoc at MIT CSAIL, where I worked with Armando Solar-Lezama.

My research interests span the areas of programming languages and formal methods; in particular, I'm interested in building practical tools and techniques that make it easier for programmers to construct secure and reliable software. My agenda is to combine the growing power of automated logical reasoning and the recent advances in program synthesis to build next-generation programming languages, in which the programmer directly states high-level system requirements (such as data invariants, resource bounds, or security policies) and the compiler takes on the error-prone task of enforcing these requirements.

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
• John Sarracino (co-advised with Sorin Lerner)

alumni:

• David Justo (master's thesis)
• Sourav Anand (master's thesis)

PAPERS

• Small-Step Live Programming by Example, Kasra Ferdowsifard, Allen Ordookhanians, Hila Peleg, Sorin Lerner, Nadia Polikarpova. UIST'20. [pdf] [preview]
• Liquid Information Flow Control, Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama. ICFP'20. [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 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

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