75 citations · 218 across the 23 of their papers we have counts for
25 papers
From Words to Code: Harnessing Data for Program Synthesis from Natural Language
Anirudh Khatry, Joyce Cahoon, Jordan Henkel +9
Creating programs to correctly manipulate data is a difficult task, as the underlying programming languages and APIs can be challenging to learn for many users who are not skilled…
Overwatch: Learning Patterns in Code Edit Sequences
Yuhao Zhang, Yasharth Bajpai, Priyanshu Gupta +8
Integrated Development Environments (IDEs) provide tool support to automate many source code editing tasks. Traditionally, IDEs use only the spatial context, i.e., the location whe…
Neurosymbolic Repair for Low-Code Formula Languages
Rohan Bavishi, Harshit Joshi, José Pablo Cambronero Sánchez +5
Most users of low-code platforms, such as Excel and PowerApps, write programs in domain-specific formula languages to carry out nontrivial tasks. Often users can write most of the…
Multi-Agent Spatial Predictive Control with Application to Drone Flocking (Extended Version)
Andreas Brandstätter, Scott A. Smolka, Scott D. Stoller +2
We introduce the novel concept of Spatial Predictive Control (SPC) to solve the following problem: given a collection of agents (e.g., drones) with positional low-level controllers…
Synchromesh: Reliable code generation from pre-trained language models
Gabriel Poesia, Oleksandr Polozov, Vu Le +4
Large pre-trained language models have been used to generate code,providing a flexible interface for synthesizing programs from natural language specifications. However, they often…
Multi-modal Program Inference: a Marriage of Pre-trainedLanguage Models and Component-based Synthesis
Kia Rahmani, Mohammad Raza, Sumit Gulwani +5
Multi-modal program synthesis refers to the task of synthesizing programs (code) from their specification given in different forms, such as a combination of natural language and ex…
A Conjecture Equivalent to the Collatz Conjecture
Ashish Tiwari
We present a formulation of the Collatz conjecture that is potentially more amenable to modeling and analysis by automated termination checking tools.
Linear Invariants for Linear Systems
Ashish Tiwari
A central question in verification is characterizing when a system has invariants of a certain form, and then synthesizing them. We say a system has a linear invariant, -LI…
Information-theoretic User Interaction: Significant Inputs for Program Synthesis
Ashish Tiwari, Arjun Radhakrishna, Sumit Gulwani +1
Programming-by-example technologies are being deployed in industrial products for real-time synthesis of various kinds of data transformations. These technologies rely on the user…
Learning Distributed Controllers for V-Formation
Shouvik Roy, Usama Mehmood, Radu Grosu +3
We show how a high-performing, fully distributed and symmetric neural V-formation controller can be synthesized from a Centralized MPC (Model Predictive Control) controller using D…
Conformance Constraint Discovery: Measuring Trust in Data-Driven Systems
Anna Fariha, Ashish Tiwari, Arjun Radhakrishna +2
The reliability and proper function of data-driven applications hinge on the data's continued conformance to the applications' initial design. When data deviates from this initial…
V-Formation via Model Predictive Control
Radu Grosu, Anna Lukina, Scott A. Smolka +3
We present recent results that demonstrate the power of viewing the problem of V-formation in a flock of birds as one of Model Predictive Control (MPC). The V-formation-MPC marriag…
Quantitative Programming by Examples
Sumit Gulwani, Kunal Pathak, Arjun Radhakrishna +2
Programming-by-Example (PBE) systems synthesize an intended program in some (relatively constrained) domain-specific language from a small number of input-output examples provided…
Neural Flocking: MPC-based Supervised Learning of Flocking Controllers
Shouvik Roy, Usama Mehmood, Radu Grosu +3
We show how a distributed flocking controller can be synthesized using deep learning from a centralized controller which generates the trajectories of the flock. Our approach is ba…
SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems
Ankush Desai, Shromona Ghosh, Sanjit A. Seshia +2
The recent drive towards achieving greater autonomy and intelligence in robotics has led to high levels of complexity. Autonomous robots increasingly depend on third party off-the-…
Adaptive Neighborhood Resizing for Stochastic Reachability in Multi-Agent Systems
Anna Lukina, Ashish Tiwari, Scott A. Smolka +1
We present DAMPC, a distributed, adaptive-horizon and adaptive-neighborhood algorithm for solving the stochastic reachability problem in multi-agent systems, in particular flocking…
Declarative vs Rule-based Control for Flocking Dynamics
Usama Mehmood, Nicola Paoletti, Dung Phan +6
The popularity of rule-based flocking models, such as Reynolds' classic flocking model, raises the question of whether more declarative flocking models are possible. This question…
Learning Task Specifications from Demonstrations
Marcell Vazquez-Chanlatte, Susmit Jha, Ashish Tiwari +2
Real world applications often naturally decompose into several sub-tasks. In many settings (e.g., robotics) demonstrations provide a natural way to specify the sub-tasks. However,…
Output Range Analysis for Deep Neural Networks
Souradeep Dutta, Susmit Jha, Sriram Sanakaranarayanan +1
Deep neural networks (NN) are extensively used for machine learning tasks such as image classification, perception and control of autonomous systems. Increasingly, these deep NNs a…
Attacking the V: On the Resiliency of Adaptive-Horizon MPC
Scott A. Smolka, Ashish Tiwari, Lukas Esterle +3
We introduce the concept of a V-formation game between a controller and an attacker, where controller's goal is to maneuver the plant (a simple model of flocking dynamics) into a V…
ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans
Anna Lukina, Lukas Esterle, Christian Hirsch +5
We introduce ARES, an efficient approximation algorithm for generating optimal plans (action sequences) that take an initial state of a Markov Decision Process (MDP) to a state who…
Synthesis of a simple self-stabilizing system
Adrià Gascón, Ashish Tiwari
With the increasing importance of distributed systems as a computing paradigm, a systematic approach to their design is needed. Although the area of formal verification has made en…
Synthesis for Polynomial Lasso Programs
Jan Leike, Ashish Tiwari
We present a method for the synthesis of polynomial lasso programs. These programs consist of a program stem, a set of transitions, and an exit condition, all in the form of algebr…
Synthesizing Switching Logic to Minimize Long-Run Cost
Susmit Jha, Sanjit A. Seshia, Ashish Tiwari
Given a multi-modal dynamical system, optimal switching logic synthesis involves generating the conditions for switching between the system modes such that the resulting hybrid sys…