Trio

System architecture of Trio

Description: Synthesizing a recursive function is challenging because recursive subexpressions should be constructed while the target function has not been fully defined yet. We address this challenge by using a new technique we call block-based pruning. A block refers to a recursion- and conditional-free expression (i.e., straight-line code) that yields an output from a particular input. We first satisfying blocks for each input-output example. Then, we prune the space of recursive programs by removing candidates that are inconsistent with the blocks.

Links: POPL 2023 paper Trio tool

Duet

System architecture of Duet (Domain-Unaware inductive synthesis via Enumeration and Top-down propagation)

Description: Bidirectional program synthesis is a new approach to program synthesis that synergistically combine the top-down propagation and bottom-up enumeration. Bottom-up numerative search is generally applicable but limited in scalability, and the top-down propagation is efficient but only works for special grammars or applications. Our key insight is combine the two approaches to obtain the best of the two worlds. We bring the power of the top-down propagation to SyGuS problems with arbitrary grammar by leveraging the bottom-up enumeration search, enabling a more scalable and general-purpose synthesis strategy.

Links: POPL 2021 paper Duet tool

Euphony

System architecture of Euphony

Description: The goal of program synthesis is to automatically synthesize a program that satisfies a given high-level specification. A central challenge in program synthesis concerns how to efficiently search for the desired program in the space of possible programs. It is well known that desired programs contain repetitive and predictable patterns. We have proposed a new approach to accelerate search-based program synthesis based on this observation. Our key insight is to learn a probabilistic model of programs and use it to guide the search.

Links: PLDI 2018 paper Euphony tool

Chisel

System architecture of Chisel
example reduced version of tar-1.14 generated by Chisel

Description: Prevalent software engineering practices have significantly increased the complexity and bloat of today’s software. This in turn has led to decreased performance and increased security vulnerabilities. The Chisel project seeks to effectively counter this trend.

Unlike conventional programming tools, which seek to preserve the program’s behavior, Chisel alters the program’s behavior by removing unnecessary functionality. The project is addressing a multitude of research problems such as how to specify the desired behavior, how to efficiently debloat programs in language-specific and language-independent ways, and what correctness guarantees to provide.

Chisel curently supports the C family of languages.

Links: Project hompeage CCS 2018 paper Chisel tool (Clang-based) Chisel tool (CIL-based) (available upon request)