76 citations · 344 across the 30 of their papers we have counts for
33 papers
Fixing the Fixpoint: A Formal Theory of Convergence Detection for Incremental Recursive Computation
Chengxi Yang, Tej Chajed, Thomas Reps
Modern incremental computation theories like DBSP have enabled efficient incrementalization of general recursive computations. To do so, they require a runtime Fixpoint Detection (…
PEA: Enhancing LLM Performance on Computational-Reasoning Tasks
Zi Wang, Shiwei Weng, Mohannad Alhanahnah +2
Large Language Models (LLMs) have exhibited remarkable capabilities across diverse domains, prompting investigations into their potential as generic reasoning engines. While recent…
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…
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…
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,…
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…
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…
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…
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-…
Neural Program Generation Modulo Static Analysis
Rohan Mukherjee, Yeming Wen, Dipak Chaudhari +3
State-of-the-art neural models of source code tend to be evaluated on the generation of individual expressions and lines of code, and commonly fail on long-horizon tasks such as th…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…
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…