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:

• SuSLik: synthesis of heap-manipulating programs with separation logic [try online]
• Synquid: program synthesis from refinement types [try online]
• Lifty: enforcing information flow security using types and synthesis [try online]

older projects:

• AutoProof: an automated deductive verifier for programs that manipulate complex object structures [try online]
• EiffelBase2: a fully verified container library
• Boogaloo: a symbolic execution engine for Boogie [try online]
• CITADEL: dynamic invariant inference meets Design-by-Contract

PAPERS

• Structuring the Synthesis of Heap-Manipulating Programs, Nadia Polikarpova, Ilya Sergey, To appear at POPL'19. [pdf]
• Automatic Synchronization for GPU Kernels, Sourav Anand, Nadia Polikarpova. FMCAD'18. [pdf]
• Enforcing Information Flow Policies with Type-Targeted Program Synthesis, Nadia Polikarpova, Jean Yang, Shachar Itzhaky, Travis Hance, Armando Solar-Lezama. In submission. [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] [tech report] [slides]
• A Fully Verified Container Library, Nadia Polikarpova, Julian Tschannen, Carlo A. Furia. FM'15. Best paper award [pdf] [repository]
  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]

PHD STUDENTS

• Shraddha Barke
• Michael James (co-advised with Ranjit Jhala)
• Tristan Knoth
• John Sarracino (co-advised with Sorin Lerner)

TEACHING

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:

2018	Constraint Solvers for the Working PL Researcher (PLMW@ICFP) [slides] [code] [code] [code]
	Type-Driven Program Synthesis (Strangeloop) [slides] [video]

program (co-)chair:

2017

iFM

program committees:

2019	PLDI
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, ECOOP
2018	PLDI