65 citations · 347 across the 17 of their papers we have counts for
20 papers
HiLDe: Intentional Code Generation via Human-in-the-Loop Decoding
Emmanuel Anaya González, Raven Rothkopf, Sorin Lerner +1
While AI programming tools hold the promise of increasing programmers' capabilities and productivity to a remarkable degree, they often exclude users from essential decision-making…
Validating AI-Generated Code with Live Programming
Kasra Ferdowsi, Ruanqianqian Huang, Michael B. James +2
AI-powered programming assistants are increasingly gaining popularity, with GitHub Copilot alone used by over a million developers worldwide. These tools are far from perfect, howe…
babble: Learning Better Abstractions with E-Graphs and Anti-Unification
David Cao, Rose Kunkel, Chandrakana Nandi +3
Library learning compresses a given corpus of programs by extracting common structure from the corpus into reusable library functions. Prior work on library learning suffers from t…
Searching Entangled Program Spaces
James Koppel, Zheng Guo, Edsko de Vries +2
Many problem domains, including program synthesis and rewrite-based optimization, require searching astronomically large spaces of programs. Existing approaches often rely on build…
Grounded Copilot: How Programmers Interact with Code-Generating Models
Shraddha Barke, Michael B. James, Nadia Polikarpova
Powered by recent advances in code-generating models, AI assistants like Github Copilot promise to change the face of programming forever. But what is this new face of programming?…
Type-Directed Program Synthesis for RESTful APIs
Zheng Guo, David Cao, Davin Tjong +3
With the rise of software-as-a-service and microservice architectures, RESTful APIs are now ubiquitous in mobile and web applications. A service can have tens or hundreds of API me…
Just-in-Time Learning for Bottom-Up Enumerative Synthesis
Shraddha Barke, Hila Peleg, Nadia Polikarpova
A key challenge in program synthesis is the astronomical size of the search space the synthesizer has to explore. In response to this challenge, recent work proposed to guide synth…
Liquid Resource Types
Tristan Knoth, Di Wang, Adam Reynolds +2
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade au…
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- Extended Version
Andreea Costea, Amy Zhu, Nadia Polikarpova +1
In program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if…
Program Synthesis by Type-Guided Abstraction Refinement
Zheng Guo, Michael James, David Justo +4
We consider the problem of type-directed component based synthesis where, given a set of (typed) components and a query type, the goal is to synthesize a term that inhabits the que…
Resource-Guided Program Synthesis
Tristan Knoth, Di Wang, Nadia Polikarpova +1
This article presents resource-guided synthesis, a technique for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The tec…
Targeted Synthesis for Programming with Data Invariants
John Sarracino, Shraddha Barke, Hila Peleg +2
Programmers frequently maintain implicit data invariants, which are relations between different data structures in a program. Traditionally, such invariants are manually enforced a…
Structuring the Synthesis of Heap-Manipulating Programs - Extended Version
Nadia Polikarpova, Ilya Sergey
This paper describes a deductive approach to synthesizing imperative programs with pointers from declarative specifications expressed in Separation Logic. Our synthesis algorithm t…
Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang +3
We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarati…
Program Synthesis from Polymorphic Refinement Types
Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama
We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specificatio…
Synthesis of Recursive ADT Transformations from Reusable Templates
Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu +2
Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user to supply a syntactic template that constrains the space of potenti…
AutoProof: Auto-active Functional Verification of Object-oriented Programs
Julian Tschannen, Carlo A. Furia, Martin Nordio +1
Auto-active verifiers provide a level of automation intermediate between fully automatic and interactive: users supply code with annotations as input while benefiting from a high l…
Flexible Invariants Through Semantic Collaboration
Nadia Polikarpova, Julian Tschannen, Carlo A. Furia +1
Modular reasoning about class invariants is challenging in the presence of dependencies among collaborating objects that need to maintain global consistency. This paper presents se…
What Good Are Strong Specifications?
Nadia Polikarpova, Carlo A. Furia, Yu Pei +2
Experience with lightweight formal methods suggests that programmers are willing to write specification if it brings tangible benefits to their usual development activities. This p…
Specifying Reusable Components
Nadia Polikarpova, Carlo A. Furia, Bertrand Meyer
Reusable software components need expressive specifications. This paper outlines a rigorous foundation to model-based contracts, a method to equip classes with strong contracts tha…