A comparative study of programmer-written and automatically inferred contracts. - Nadia Polikarpova; Ilinca Ciupa; Bertrand Meyer 001 (ISSTA, 2009)

Specifying Reusable Components. - Nadia Polikarpova; Carlo A. Furia; Bertrand Meyer 001 (VSTTE, 2010)

The 1st Verified Software Competition: Experience Report. - Vladimir Klebanov; Peter Müller 001; Natarajan Shankar; Gary T. Leavens; Valentin Wüstholz; Eyad Alkassar; Rob Arthan; Derek Bronish; Rod Chapman; Ernie Cohen; Mark A. Hillebrand; Bart Jacobs 002; et al. (FM, 2011)

The COST IC0701 Verification Competition 2011. - Thorsten Bormer; Marc Brockschmidt; Dino Distefano; Gidon Ernst; Jean-Christophe Filliâtre; Radu Grigore; Marieke Huisman; Vladimir Klebanov; Claude Marché; Rosemary Monahan; Wojciech Mostowski; Nadia Polikarpova; et al. (FoVeOOS, 2011)

Verifying Implementations of Security Protocols by Refinement. - Nadia Polikarpova; Michal Moskal (VSTTE, 2012)

What good are strong specifications? - Nadia Polikarpova; Carlo A. Furia; Yu Pei 001; Yi Wei 001; Bertrand Meyer 001 (ICSE, 2013)

To Run What No One Has Run Before: Executing an Intermediate Verification Language. - Nadia Polikarpova; Carlo A. Furia; Scott West (RV, 2013)

Verified Calculations. - K. Rustan M. Leino; Nadia Polikarpova (VSTTE, 2013)

Flexible Invariants through Semantic Collaboration. - Nadia Polikarpova; Julian Tschannen; Carlo A. Furia; Bertrand Meyer 001 (FM, 2014)

Specified and verified reusable components. - Nadia Polikarpova (2014)

Program Synthesis from Polymorphic Refinement Types. - Nadia Polikarpova; Armando Solar-Lezama (CoRR, 2015)

Program synthesis from polymorphic refinement types. - Nadia Polikarpova; Ivan Kuraj; Armando Solar-Lezama (PLDI, 2016)

Type-Driven Repair for Information Flow Security. - Nadia Polikarpova; Jean Yang 001; Shachar Itzhaky; Armando Solar-Lezama (CoRR, 2016)

Synthesis of Recursive ADT Transformations from Reusable Templates. - Jeevana Priya Inala; Nadia Polikarpova; Xiaokang Qiu; Benjamin S. Lerner; Armando Solar-Lezama (TACAS (1), 2017)

AutoProof: auto-active functional verification of object-oriented programs. - Carlo A. Furia; Martin Nordio; Nadia Polikarpova; Julian Tschannen (Int. J. Softw. Tools Technol. Transf., 2017)

Automatic Synchronization for GPU Kernels. - Sourav Anand; Nadia Polikarpova (FMCAD, 2018)

A fully verified container library. - Nadia Polikarpova; Julian Tschannen; Carlo A. Furia (Formal Aspects Comput., 2018)

Constraint-based Learning of Phonological Processes. - Shraddha Barke; Rose Kunkel; Nadia Polikarpova; Eric Meinhardt; Eric Bakovic; Leon Bergen (EMNLP/IJCNLP (1), 2019)

SuSLik: Synthesis of Safe Pointer-Manipulating Programs (Invited Tutorial). - Nadia Polikarpova (FMCAD, 2019)

Resource-guided program synthesis. - Tristan Knoth; Di Wang 017; Nadia Polikarpova; Jan Hoffmann 002 (PLDI, 2019)

Targeted Synthesis for Programming with Data Invariants. - John Sarracino; Shraddha Barke; Nadia Polikarpova; Sorin Lerner (CoRR, 2019)

Structuring the synthesis of heap-manipulating programs. - Nadia Polikarpova; Ilya Sergey (Proc. ACM Program. Lang., 2019)

Perfect Is the Enemy of Good: Best-Effort Program Synthesis. - Hila Peleg; Nadia Polikarpova (ECOOP, 2020)

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers. - Andreea Costea; Amy Zhu; Nadia Polikarpova; Ilya Sergey (ESOP, 2020)

Small-Step Live Programming by Example. - Kasra Ferdowsifard; Allen Ordookhanians; Hila Peleg; Sorin Lerner; Nadia Polikarpova (UIST, 2020)

Concise Read-Only Specifications for Better Synthesis of Programs with Pointers - Extended Version. - Andreea Costea; Amy Zhu; Nadia Polikarpova; Ilya Sergey (CoRR, 2020)

Perfect is the Enemy of Good: Best-Effort Program Synthesis (Artifact). - Hila Peleg; Nadia Polikarpova (Dagstuhl Artifacts Ser., 2020)

Just-in-time learning for bottom-up enumerative synthesis. - Shraddha Barke; Hila Peleg; Nadia Polikarpova (Proc. ACM Program. Lang., 2020)

Program synthesis by type-guided abstraction refinement. - Zheng Guo 003; Michael James 003; David Justo; Jiaxiao Zhou; Ziteng Wang; Ranjit Jhala; Nadia Polikarpova (Proc. ACM Program. Lang., 2020)

Digging for fold: synthesis-aided API discovery for Haskell. - Michael B. James; Zheng Guo 003; Ziteng Wang; Shivani Doshi; Hila Peleg; Ranjit Jhala; Nadia Polikarpova (Proc. ACM Program. Lang., 2020)

Liquid resource types. - Tristan Knoth; Di Wang 017; Adam Reynolds; Jan Hoffmann 002; Nadia Polikarpova (Proc. ACM Program. Lang., 2020)

Liquid information flow control. - Nadia Polikarpova; Deian Stefan; Jean Yang 001; Shachar Itzhaky; Travis Hance; Armando Solar-Lezama (Proc. ACM Program. Lang., 2020)

Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities - (Invited Paper). - Shachar Itzhaky; Hila Peleg; Nadia Polikarpova; Reuben N. S. Rowe; Ilya Sergey (CAV (1), 2021)

Learning part-based abstractions for visual object concepts. - Haoliang Wang; Nadia Polikarpova; Judith E. Fan (CogSci, 2021)

Theory Acquisition as Constraint-Based Program Synthesis. - Haoliang Wang; Ed Vul; Nadia Polikarpova; Judith E. Fan (CogSci, 2021)

Synthesis of Safe Pointer-Manipulating Programs (Invited Talk). - Nadia Polikarpova (ITP, 2021)

STORM: Refinement Types for Secure Web Applications. - Nico Lehmann; Rose Kunkel; Jordan Brown; Jean Yang 001; Niki Vazou; Nadia Polikarpova; Deian Stefan; Ranjit Jhala (OSDI, 2021)

Cyclic program synthesis. - Shachar Itzhaky; Hila Peleg; Nadia Polikarpova; Reuben N. S. Rowe; Ilya Sergey (PLDI, 2021)

Synthesis of web layouts from examples. - Dylan Lukes; John Sarracino; Cora Coleman; Hila Peleg; Sorin Lerner; Nadia Polikarpova (ESEC/SIGSOFT FSE, 2021)

LooPy: interactive program synthesis with control structures. - Kasra Ferdowsifard; Shraddha Barke; Hila Peleg; Sorin Lerner; Nadia Polikarpova (Proc. ACM Program. Lang., 2021)

Certifying the synthesis of heap-manipulating programs. - Yasunari Watanabe; Kiran Gopinathan; George Pîrlea; Nadia Polikarpova; Ilya Sergey (Proc. ACM Program. Lang., 2021)

Towards A Polyglot Framework for Factorized ML. - David Justo; Shaoqing Yi; Lukas Stadler; Nadia Polikarpova; Arun Kumar 001 (Proc. VLDB Endow., 2021)

Type-directed program synthesis for RESTful APIs. - Zheng Guo 003; David Cao; Davin Tjong; Jean Yang 001; Cole Schlesinger; Nadia Polikarpova (PLDI, 2022)

Optimizing consistency for partially replicated data stores. - Ivan Kuraj; Armando Solar-Lezama; Nadia Polikarpova (PPoPP, 2022)

Searching entangled program spaces. - James Koppel; Zheng Guo 003; Edsko de Vries; Armando Solar-Lezama; Nadia Polikarpova (Proc. ACM Program. Lang., 2022)

COLDECO: An End User Spreadsheet Inspection Tool for AI-Generated Code. - Kasra Ferdowsi; Jack Williams 001; Ian Drosos; Andrew D. Gordon 001; Carina Negreanu; Nadia Polikarpova; Advait Sarkar; Benjamin Zorn 001 (VL/HCC, 2023)

Live Exploration of AI-Generated Programs. - Kasra Ferdowsi; Ruanqianqian (Lisa) Huang; Michael B. James; Nadia Polikarpova; Sorin Lerner (CoRR, 2023)

Leveraging Rust Types for Program Synthesis. - Jonás Fiala; Shachar Itzhaky; Peter Müller 001; Nadia Polikarpova; Ilya Sergey (Proc. ACM Program. Lang., 2023)

babble: Learning Better Abstractions with E-Graphs and Anti-unification. - David Cao; Rose Kunkel; Chandrakana Nandi; Max Willsey; Zachary Tatlock; Nadia Polikarpova (Proc. ACM Program. Lang., 2023)

Grounded Copilot: How Programmers Interact with Code-Generating Models. - Shraddha Barke; Michael B. James; Nadia Polikarpova (Proc. ACM Program. Lang., 2023)

Validating AI-Generated Code with Live Programming. - Kasra Ferdowsi; Ruanqianqian (Lisa) Huang; Michael B. James; Nadia Polikarpova; Sorin Lerner (CHI, 2024)

Solving Data-centric Tasks using Large Language Models. - Shraddha Barke; Christian Pölitz; Carina Negreanu; Benjamin Zorn 001; José Cambronero; Andrew D. Gordon 001; Vu Le 002; Elnaz Nouri; Nadia Polikarpova; Advait Sarkar; Brian Slininger; Neil Toronto; et al. (NAACL-HLT (Findings), 2024)

HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis. - Shraddha Barke; Emmanuel Anaya Gonzalez; Saketh Ram Kasibatla; Taylor Berg-Kirkpatrick; Nadia Polikarpova (NeurIPS, 2024)

Grammar-Aligned Decoding. - Kanghee Park; Jiayu Wang; Taylor Berg-Kirkpatrick; Nadia Polikarpova; Loris D'Antoni (NeurIPS, 2024)

Laurel: Generating Dafny Assertions Using Large Language Models. - Eric Mugnier; Emmanuel Anaya Gonzalez; Ranjit Jhala; Nadia Polikarpova; Yuanyuan Zhou 001 (CoRR, 2024)

Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis. - Ruyi Ji; Yuwei Zhao; Nadia Polikarpova; Yingfei Xiong 001; Zhenjiang Hu (Proc. ACM Program. Lang., 2024)

CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs. - Cole Kurashige; Ruyi Ji; Aditya Giridharan; Mark Barbone; Daniel Noor; Shachar Itzhaky; Ranjit Jhala; Nadia Polikarpova (Proc. ACM Program. Lang., 2024)

Artifact for PLDI'24: Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis. - Ruyi Ji; Yuwei Zhao; Nadia Polikarpova; Yingfei Xiong 001; Zhenjiang Hu (Zenodo, 2024)

Artifact for PLDI'24: Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis. - Ruyi Ji; Yuwei Zhao; Nadia Polikarpova; Yingfei Xiong 001; Zhenjiang Hu (Zenodo, 2024)

Artifact for PLDI'24: Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis. - Ruyi Ji; Yuwei Zhao; Nadia Polikarpova; Yingfei Xiong 001; Zhenjiang Hu (Zenodo, 2024)

Peepco: Batch-Based Consistency Optimization. - Ivan Kuraj; John K. Feser; Nadia Polikarpova; Armando Solar-Lezama (Proc. ACM Program. Lang., 2025)

Laurel: Unblocking Automated Verification with Large Language Models. - Eric Mugnier; Emmanuel Anaya Gonzalez; Nadia Polikarpova; Ranjit Jhala; Yuanyuan Zhou 001 (Proc. ACM Program. Lang., 2025)

HiLDe: Intentional Code Generation via Human-in-the-Loop Decoding. - Emmanuel Anaya Gonzalez; Raven Rothkopf; Sorin Lerner; Nadia Polikarpova (CoRR, 2025)