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.
PROJECTS
active projects:
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:
alumni:
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
winter 2021 |
CSE 291: Program Synthesis |
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:
program (co-)chair:
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: