Nadia Polikarpova

polikarn [at] csail.mit.edu

32 Vassar street, 32-G714
Cambridge, MA 02139, USA

cv | research statement | teaching statement | diversity statement
google scholar | bitbucket | twitter

This page is outdated. I've moved to UCSD.

I am a postdoc at MIT CSAIL, where I work with Armando Solar-Lezama. I completed my PhD in 2014 at ETH Zurich (Switzerland), under the supervision of Bertrand Meyer. During my doctoral studies I was a research intern at Microsoft Research Redmond, working with Michał Moskal. I received my Bachelor's and Master's degrees in Applied Mathematics and Informatics from ITMO University (Saint Petersburg, Russia).

My research interests are in program verification and synthesis. Here are some of my current and past projects:

• Synquid: program synthesis from refinement types [try online]
• LIFTy: enforcing information flow security using types and synthesis [try online]
• 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

Publications

• Type-Driven Repair for Information Flow Security, Nadia Polikarpova, Jean Yang, Shachar Itzhaky, Armando Solar-Lezama. In submission. [pdf] [supplementary material]
• 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]
• 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]

Professional Activities

I'm a Program Co-chair of iFM'17.

Program Committees: POPL'18, CAV'17, APLAS'16, FTfJP'16, SYNT'16, VSTTE'16, TAP'16, iFM'16, FESCA'16, VMCAI'16, PSI’15, FTfJP'15, FESCA'15, RV'14, FESCA'14.

Artifact Evaluation Committees: POPL'17, ESEC/FSE'15.

I also have reviewed articles for Formal Aspects of Computing and Journal of Functional Programming.

I helped organize RV'14 as a Tutorials and Publication Chair, and ESEC/FSE'13 as a Deputy General Chair (for which I got the ACM SIGSOFT Recognition of Services Award). I also served as Publicity Chair for the LASER Summer School in 2011-2014.