84 citations · 356 across the 59 of their papers we have counts for
32 papers · 1 filter
Optimal Predicate Pushdown Synthesis
Robert Zhang, Eric Hayden Campbell, Dixin Tang +1
Predicate pushdown is a long-standing performance optimization that filters data as early as possible in a computational workflow. In modern data pipelines, this transformation is…
Choose, Don't Label: Multiple-Choice Query Synthesis for Program Disambiguation
Celeste Barnaby, Danny Ding, Osbert Bastani +1
High-level specifications of code are inherently ambiguous, and prior systems have explored interactive techniques to help users clarify their intent and resolve such ambiguities.…
Active Learning for Neurosymbolic Program Synthesis
Celeste Barnaby, Qiaochu Chen, Ramya Ramalingam +2
The goal of active learning for program synthesis is to synthesize the desired program by asking targeted questions that minimize user interaction. While prior work has explored ac…
Probabilistic Inference for Datalog with Correlated Inputs
Jingbo Wang, Shashin Halalingaiah, Weiyi Chen +2
Probabilistic extensions of logic programming languages, such as ProbLog, integrate logical reasoning with probabilistic inference to evaluate probabilities of output relations; ho…
Homomorphism Calculus for User-Defined Aggregations
Ziteng Wang, Ruijie Fang, Linus Zheng +2
Data processing frameworks like Apache Spark and Flink provide built-in support for user-defined aggregation functions (UDAFs), enabling the integration of domain-specific logic. H…
Graphiti: Bridging Graph and Relational Database Queries
Yang He, Ruijie Fang, Isil Dillig +1
This paper presents an automated reasoning technique for checking equivalence between graph database queries written in Cypher and relational queries in SQL. To formalize a suitabl…
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Yutong Xin, Jimmy Xin, Gabriel Poesia +3
Enabling more concise and modular proofs is essential for advancing formal reasoning using interactive theorem provers (ITPs). Since many ITPs, such as Rocq and Lean, use tactic-st…
From Batch to Stream: Automatic Generation of Online Algorithms
Ziteng Wang, Shankara Pailoor, Aaryan Prakash +2
Online streaming algorithms, tailored for continuous data processing, offer substantial benefits but are often more intricate to design than their offline counterparts. This paper…
Data Extraction via Semantic Regular Expression Synthesis
Qiaochu Chen, Arko Banerjee, Çağatay Demiralp +2
Many data extraction tasks of practical relevance require not only syntactic pattern matching but also semantic reasoning about the content of the underlying text. While regular ex…
ImageEye: Batch Image Processing Using Program Synthesis
Celeste Barnaby, Qiaochu Chen, Roopsha Samanta +1
This paper presents a new synthesis-based approach for batch image processing. Unlike existing tools that can only apply global edits to the entire image, our method can apply fine…
Type-Directed Synthesis of Visualizations from Natural Language Queries
Qiaochu Chen, Shankara Pailoor, Celeste Barnaby +4
We propose a new technique based on program synthesis for automatically generating visualizations from natural language queries. Our method parses the natural language query into a…
Metric Program Synthesis
John Feser, Isil Dillig, Armando Solar-Lezama
We present a new domain-agnostic synthesis technique for generating programs from input-output examples. Our method, called metric program synthesis, relaxes the well-known observa…
Automated Transpilation of Imperative to Functional Code using Neural-Guided Program Synthesis (Extended Version)
Benjamin Mariano, Yanju Chen, Yu Feng +2
While many mainstream languages such as Java, Python, and C# increasingly incorporate functional APIs to simplify programming and improve parallelization/performance, there are no…
Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors (Extended Version)
Kostas Ferles, Benjamin Sepanski, Rahul Krishnan +2
A monitor is a widely-used concurrent programming abstraction that encapsulates all shared state between threads. Monitors can be classified as being either implicit or explicit de…
Bottom-up Synthesis of Recursive Functional Programs using Angelic Execution
Anders Miltner, Adrian Trejo Nuñez, Ana Brendel +2
We present a novel bottom-up method for the synthesis of functional recursive programs. While bottom-up synthesis techniques can work better than top-down methods in certain settin…
Web Question Answering with Neurosymbolic Program Synthesis
Qiaochu Chen, Aaron Lamoreaux, Xinyu Wang +3
In this paper, we propose a new technique based on program synthesis for extracting information from webpages. Given a natural language query and a few labeled webpages, our method…
Verifying Correct Usage of Context-Free API Protocols (Extended Version)
Kostas Ferles, Jon Stephens, Isil Dillig
Several real-world libraries (e.g., reentrant locks, GUI frameworks, serialization libraries) require their clients to use the provided API in a manner that conforms to a context-f…
LambdaNet: Probabilistic Type Inference using Graph Neural Networks
Jiayi Wei, Maruth Goyal, Greg Durrett +1
As gradual typing becomes increasingly popular in languages like Python and TypeScript, there is a growing need to infer type annotations automatically. While type annotations help…
Visualization by Example
Chenglong Wang, Yu Feng, Rastislav Bodik +2
While visualizations play a crucial role in gaining insights from data, generating useful visualizations from a complex dataset is far from an easy task. Besides understanding the…
Multi-modal Synthesis of Regular Expressions
Qiaochu Chen, Xinyu Wang, Xi Ye +2
In this paper, we propose a multi-modal synthesis technique for automatically constructing regular expressions (regexes) from a combination of examples and natural language. Using…
Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
Greg Anderson, Shankara Pailoor, Isil Dillig +1
In recent years, the notion of local robustness (or robustness for short) has emerged as a desirable property of deep neural networks. Intuitively, robustness means that small pert…
Synthesizing Database Programs for Schema Refactoring
Yuepeng Wang, James Dong, Rushi Shah +1
Many programs that interact with a database need to undergo schema refactoring several times during their life cycle. Since this process typically requires making significant chang…
Formal Specification and Verification of Smart Contracts for Azure Blockchain
Yuepeng Wang, Shuvendu K. Lahiri, Shuo Chen +4
Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. This paper studies the safety and security of smart contracts in the \emph{Azure…
Relational Program Synthesis
Yuepeng Wang, Xinyu Wang, Isil Dillig
This paper proposes relational program synthesis, a new problem that concerns synthesizing one or more programs that collectively satisfy a relational specification. As a dual of r…