33 citations · 166 across the 51 of their papers we have counts for
25 papers · 1 filter
Language-Based Agent Control
Timothy Zhou, Loris D'Antoni, Nadia Polikarpova
This paper introduces language-based agent control (LBAC), a new programming model for agentic applications that brings techniques from programming languages and language-based sec…
Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
Xuanyu Peng, Dominic Kennedy, Yuyou Fan +3
Static analyses play a fundamental role during compilation: they discover facts that are true in all executions of the code being compiled, and then these facts are used to justify…
ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models
Shaan Nagy, Timothy Zhou, Nadia Polikarpova +1
Language models (LMs) can generate code but cannot guarantee its correctness$\unicode{x2014}$often producing outputs that violate type safety, program invariants, or other semantic…
Semantics of Sets of Programs
Jinwoo Kim, Shaan Nagy, Thomas Reps +1
Applications like program synthesis sometimes require proving that a property holds for all of the infinitely many programs described by a grammar - i.e., an inductively defined se…
Synthesizing Formal Semantics from Executable Interpreters
Jiangyi Liu, Charlie Murphy, Anvay Grover +3
Program verification and synthesis frameworks that allow one to customize the language in which one is interested typically require the user to provide a formally defined semantics…
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
Keith J. C. Johnson, Rahul Krishnan, Thomas Reps +1
In top-down enumeration for program synthesis, abstraction-based pruning uses an abstract domain to approximate the set of possible values that a partial program, when completed, c…
Verifying Solutions to Semantics-Guided Synthesis Problems
Charlie Murphy, Keith Johnson, Thomas Reps +1
Semantics-Guided Synthesis (SemGuS) provides a framework to specify synthesis problems in a solver-agnostic and domain-agnostic way, by allowing a user to provide both the syntax a…
LOUD: Synthesizing Strongest and Weakest Specifications
Kanghee Park, Xuanyu Peng, Loris D'Antoni
This paper tackles the problem of synthesizing specifications for nondeterministic programs. For such programs, useful specifications can capture demonic properties, which hold for…
The SemGuS Toolkit
Keith J. C. Johnson, Andrew Reynolds, Thomas Reps +1
Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS fo…
Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
Shaan Nagy, Jinwoo Kim, Thomas Reps +1
Automated verification of all members of a (potentially infinite) set of programs has the potential to be useful in program synthesis, as well as in verification of dynamically loa…
Modular System Synthesis
Kanghee Park, Keith J. C. Johnson, Loris D'Antoni +1
This paper describes a way to improve the scalability of program synthesis by exploiting modularity: larger programs are synthesized from smaller programs. The key issue is to make…
Synthesizing Specifications
Kanghee Park, Loris D'Antoni, Thomas Reps
Every program should be accompanied by a specification that describes important aspects of the code's behavior, but writing good specifications is often harder than writing the cod…
Unrealizability Logic
Jinwoo Kim, Loris D'Antoni, Thomas Reps
We consider the problem of establishing that a program-synthesis problem is unrealizable (i.e., has no solution in a given search space of programs). Prior work on unrealizability…
P4BID: Information Flow Control in P4
Karuna Grewal, Loris D'Antoni, Justin Hsu
Modern programmable network switches can implement custom applications using efficient packet processing hardware, and the programming language P4 provides high-level constructs to…
Synthesizing Abstract Transformers
Pankaj Kumar Kalita, Sujit Kumar Muduli, Loris D'Antoni +2
This paper addresses the problem of creating abstract transformers automatically. The method we present automates the construction of static analyzers in a fashion similar to the w…
Synthesis with Asymptotic Resource Bounds
Qinheping Hu, John Cyphert, Loris D'Antoni +1
We present a method for synthesizing recursive functions that satisfy both a functional specification and an asymptotic resource bound. Prior methods for synthesis with a resource…
Semantics-Guided Synthesis
Jinwoo Kim, Qinheping Hu, Loris D'Antoni +1
This paper develops a new framework for program synthesis, called semantics-guided synthesis (SemGuS), that allows a user to provide both the syntax and the semantics for the const…
Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems
Qinheping Hu, John Cyphert, Loris D'Antoni +1
We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e., has no solution). We formulate the problem of prov…
Proving Data-Poisoning Robustness in Decision Trees
Samuel Drews, Aws Albarghouthi, Loris D'Antoni
Machine learning models are brittle, and small changes in the training data can result in different predictions. We study the problem of proving that a prediction is robust to data…
Efficient Synthesis with Probabilistic Constraints
Samuel Drews, Aws Albarghouthi, Loris D'Antoni
We consider the problem of synthesizing a program given a probabilistic specification of its desired behavior. Specifically, we study the recent paradigm of distribution-guided ind…
Proving Unrealizability for Syntax-Guided Synthesis
Qinheping Hu, Jason Breck, John Cyphert +2
Proving Unrealizability for Syntax-Guided Synthesis We consider the problem of automatically establishing that a given syntax-guided-synthesis (SyGuS) problem is unrealizable (i.e.…
Program Repair via Direct State Manipulation
Qinheping Hu, Isaac Evavold, Roopsha Samanta +2
The goal of program repair is to automatically fix programs to meet a specification. We propose a new specification mechanism, direct manipulation, in which the programmer can visu…
Quantifying Program Bias
Aws Albarghouthi, Loris D'Antoni, Samuel Drews +1
With the range and sensitivity of algorithmic decisions expanding at a break-neck speed, it is imperative that we aggressively investigate whether programs are biased. We propose a…
Fairness as a Program Property
Aws Albarghouthi, Loris D'Antoni, Samuel Drews +1
We explore the following question: Is a decision-making program fair, for some useful definition of fairness? First, we describe how several algorithmic fairness questions can be p…