Publications (49)
Shipwright: A Human-in-the-Loop System for Dockerfile Repair
Jordan Henkel, Denini Silva, Leopoldo Teixeira +2
Docker is a tool for lightweight OS-level virtualization. Docker images are created by performing a build, controlled by a source-level artifact called a Dockerfile. We studied Doc…
Sound Probabilistic Inference via Guide Types
Di Wang, Jan Hoffmann, Thomas Reps
Probabilistic programming languages aim to describe and automate Bayesian modeling and inference. Modern languages support programmable inference, which allows users to customize i…
Enabling Open-World Specification Mining via Unsupervised Learning
Jordan Henkel, Shuvendu K. Lahiri, Ben Liblit +1
Many programming tasks require using both domain-specific code and well-established patterns (such as routines concerned with file IO). Together, several small patterns combine to…
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…
Weighted Context-Free-Language Ordered Binary Decision Diagrams
Meghana Sistla, Swarat Chaudhuri, Thomas Reps
This paper presents a new data structure, called \emph{Weighted Context-Free-Language Ordered BDDs} (WCFLOBDDs), which are a hierarchically structured decision diagram, akin to Wei…
SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
Nengkun Yu, Jens Palsberg, Thomas Reps
Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Despite extensive research, existing verification t…
Central Moment Analysis for Cost Accumulators in Probabilistic Programs
Di Wang, Jan Hoffmann, Thomas Reps
For probabilistic programs, it is usually not possible to automatically derive exact information about their properties, such as the distribution of states at a given program point…
MHA-RAG: Improving Efficiency, Accuracy, and Consistency by Encoding Exemplars as Soft Prompts
Abhinav Jain, Xinyu Yao, Thomas Reps +1
Adapting Foundation Models to new domains with limited training data is challenging and computationally expensive. While prior work has demonstrated the effectiveness of using doma…
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…
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.…
Templates and Recurrences: Better Together
Jason Breck, John Cyphert, Zachary Kincaid +1
This paper is the confluence of two streams of ideas in the literature on generating numerical invariants, namely: (1) template-based methods, and (2) recurrence-based methods. A t…
Lightweight, Multi-Stage, Compiler-Assisted Application Specialization
Mohannad Alhanahnah, Rithik Jain, Vaibhav Rastogi +2
Program debloating aims to enhance the performance and reduce the attack surface of bloated applications. Several techniques have been recently proposed to specialize programs. The…
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…
Manjushri: A Tool for Equivalence Checking of Quantum Circuits
Xuan Du Trinh, Meghana Sistla, Nengkun Yu +1
Verifying whether two quantum circuits are equivalent is a central challenge in the compilation and optimization of quantum programs. We introduce \textsc{Manjushri}, a new automat…
Simulating reachability using first-order logic with applications to verification of linked data structures
Tal Lev-Ami, Neil Immerman, Thomas Reps +3
This paper shows how to harness existing theorem provers for first-order logic to automatically verify safety properties of imperative programs that perform dynamic storage allocat…
Optimal Symbolic Bound Synthesis
John Cyphert, Yotam Feldman, Zachary Kincaid +1
The problem of finding a constant bound on a term given a set of assumptions has wide applications in optimization as well as program analysis. However, in many contexts the object…
On The Finetuning of MLIPs Through the Lens of Iterated Maps With BPTT
Evan Dramko, Yizhi Zhu, Aleksandar Krivokapic +4
Accurate structural relaxation is critical for advanced materials design. Traditional approaches built on physics-derived first-principles calculations are computationally expensiv…
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…
Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces
Jordan Henkel, Shuvendu K. Lahiri, Ben Liblit +1
With the rise of machine learning, there is a great deal of interest in treating programs as data to be fed to learning algorithms. However, programs do not start off in a form tha…
Counterexample Guided Learning in the Large using Reasoning Agents
Hongyi Liu, Frederic Sala, Thomas Reps +1
LLMs and LLM agents should improve when given feedback, but identifying when they are able to do so is difficult: feedback is heterogeneous, domain-specific, and difficult to contr…
Semantic Robustness of Models of Source Code
Goutham Ramakrishnan, Jordan Henkel, Zi Wang +3
Deep neural networks are vulnerable to adversarial examples - small input perturbations that result in incorrect predictions. We study this problem for models of source code, where…
A Generating-Extension-Generator for Machine Code
Michael Vaughn, Thomas Reps
The problem of "debloating" programs for security and performance purposes has begun to see increased attention. Of particular interest in many environments is debloating commodity…
Prompt Tuning Strikes Back: Customizing Foundation Models with Low-Rank Prompt Adaptation
Abhinav Jain, Swarat Chaudhuri, Thomas Reps +1
Parameter-Efficient Fine-Tuning (PEFT) has become the standard for customising Foundation Models (FMs) to user-specific downstream tasks. However, typical PEFT methods require stor…
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…
Coarse-Tuning Models of Code with Reinforcement Learning Feedback
Abhinav Jain, Chima Adiole, Swarat Chaudhuri +2
Large Language Models (LLMs) pre-trained on code have recently emerged as the dominant approach to program synthesis. However, these models are trained using next-token prediction,…
TOFU: Target-Oriented FUzzer
Zi Wang, Ben Liblit, Thomas Reps
Program fuzzing---providing randomly constructed inputs to a computer program---has proved to be a powerful way to uncover bugs, find security vulnerabilities, and generate test in…
Newtonian Program Analysis of Probabilistic Programs
Di Wang, Thomas Reps
Due to their quantitative nature, probabilistic programs pose non-trivial challenges for designing compositional and efficient program analyses. Many analyses for probabilistic pro…
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…
Symbolic Quantum Simulation with Quasimodo
Meghana Sistla, Swarat Chaudhuri, Thomas Reps
The simulation of quantum circuits on classical computers is an important problem in quantum computing. Such simulation requires representations of distributions over very large se…
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…
Efficient Cost Bounds with Linear Maps
David M Kahn, Jan Hoffmann, Thomas Reps +1
The Automatic Amortized Resource Analysis (AARA) derives program-execution cost bounds using types. To do so, AARA often makes use of cost-free types, which are critical for the co…
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…
Software Model Checking via Summary-Guided Search (Extended Version)
Ruijie Fang, Zachary Kincaid, Thomas Reps
In this work, we describe a new software model-checking algorithm called GPS. GPS treats the task of model checking a program as a directed search of the program states, guided by…
slash: A Technique for Static Configuration-Logic Identification
Mohannad Alhanahnah, Philipp Schubert, Thomas Reps +2
Researchers have recently devised tools for debloating software and detecting configuration errors. Several of these tools rely on the observation that programs are composed of an…
CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams
Meghana Sistla, Swarat Chaudhuri, Thomas Reps
This paper presents a new compressed representation of Boolean functions, called CFLOBDDs (for Context-Free-Language Ordered Binary Decision Diagrams). They are essentially a plug-…
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Nengkun Yu, Xuan Du Trinh, Thomas Reps
This paper concerns the problem of checking if two shallow (i.e., constant-depth) quantum circuits perform equivalent computations. Equivalence checking is a fundamental correctnes…
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…
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…
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…
Expected-Cost Analysis for Probabilistic Programs and Semantics-Level Adaption of Optional Stopping Theorems
Di Wang, Jan Hoffmann, Thomas Reps
In this article, we present a semantics-level adaption of the Optional Stopping Theorem, sketch an expected-cost analysis as its application, and survey different variants of the O…
Learning from, Understanding, and Supporting DevOps Artifacts for Docker
Jordan Henkel, Christian Bird, Shuvendu K. Lahiri +1
With the growing use of DevOps tools and frameworks, there is an increased need for tools and techniques that support more than code. The current state-of-the-art in static develop…
A Dataset of Dockerfiles
Jordan Henkel, Christian Bird, Shuvendu K. Lahiri +1
Dockerfiles are one of the most prevalent kinds of DevOps artifacts used in industry. Despite their prevalence, there is a lack of sophisticated semantics-aware static analysis of…
Synthesizing Abstract Transformers for Reduced-Product Domains
Pankaj Kumar Kalita, Thomas Reps, Subhajit Roy
Recently, we showed how to apply program-synthesis techniques to create abstract transformers in a user-provided domain-specific language (DSL) L (i.e., ''L-transformers"). However…
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…
Source Forager: A Search Engine for Similar Source Code
Vineeth Kashyap, David Bingham Brown, Ben Liblit +2
Developers spend a significant amount of time searching for code: e.g., to understand how to complete, correct, or adapt their own code for a new context. Unfortunately, the state…
ADAPT: Lightweight, Long-Range Machine Learning Force Fields Without Graphs
Evan Dramko, Yihuang Xiong, Yizhi Zhu +4
Point defects play a central role in driving the properties of materials. First-principles methods are widely used to compute defect energetics and structures, including at scale f…
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…
The Best of Times, the Worst of Times: Moment-Based Analysis of Probabilistic Cost Structures
Chenyu Zhou, Di Wang, Thomas Reps
The paper introduces a compositional static analysis that computes mean, variance, and higher moments of cost distributions for probabilistic programs whose costs involve additive,…
Polynomial Bounds of CFLOBDDs against BDDs
Xusheng Zhi, Thomas Reps
Binary Decision Diagrams (BDDs) are widely used for the representation of Boolean functions. Context-Free-Language Ordered Decision Diagrams (CFLOBDDs) are a plug-compatible replac…