Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 PLDI
Thu 24 Jun 2021 09:30 - 09:35 at PLDI-A - Talks 3A: Analysis and Synthesis
Thu 24 Jun 2021 21:30 - 21:35 at PLDI-A - Talks 3A: Analysis and Synthesis

In recent years, researchers have explored component-based synthesis, which aims to automatically construct programs that operate by composing calls to existing APIs. However, prior work has not considered efficient synthesis of methods with side effects, e.g., web app methods that update a database. In this paper, we introduce RbSyn, a novel type- and effect-guided synthesis tool for Ruby. An RbSyn synthesis goal is specified as the type for the target method and a series of test cases it must pass. RbSyn works by recursively generating well-typed candidate method bodies whose write effects match the read effects of the test case assertions. After finding a set of candidates that separately satisfy each test, RbSyn synthesizes a solution that branches to execute the correct candidate code under the appropriate conditions. We formalize RbSyn on a core, object-oriented language $\lambda_{syn}$ and describe how the key ideas of the model are scaled-up in our implementation for Ruby. We evaluated RbSyn on 19 benchmarks, 12 of which come from popular, open-source Ruby apps. We found that RbSyn synthesizes correct solutions for all benchmarks, with 15 benchmarks synthesizing in under 9 seconds, while the slowest benchmark takes 83 seconds. Using observed reads to guide synthesize is effective: using type-guidance alone times out on 10 of 12 app benchmarks. We also found that using less precise effect annotations leads to worse synthesis performance. In summary, we believe type- and effect-guided synthesis is an important step forward in synthesis of effectful methods from test cases.

Thu 24 Jun

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 09:40
Talks 3A: Analysis and SynthesisPLDI at PLDI-A +12h
09:00
5m
Talk
Trace-Based Control-Flow Analysis
PLDI
DOI
09:05
5m
Talk
Demanded Abstract Interpretation
PLDI
Benno Stein University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon, Manu Sridharan University of California at Riverside
DOI
09:10
5m
Talk
Unleashing the Hidden Power of Compiler Optimization on Binary Code Difference: An Empirical Study
PLDI
Xiaolei Ren University of Texas at Arlington, Michael Ho University of Texas at Arlington, Jiang Ming University of Texas at Arlington, Jeff Yu Lei University of Texas at Arlington, Li Li Monash University
DOI
09:15
5m
Talk
Chianina: An Evolving Graph System for Flow- and Context-Sensitive Analyses of Million Lines of C Code
PLDI
Zhiqiang Zuo Nanjing University, Yiyu Zhang Nanjing University, Qiuhong Pan Nanjing University, Shenming Lu Nanjing University, Yue Li Nanjing University, Linzhang Wang Nanjing University, Xuandong Li Nanjing University, Guoqing Harry Xu University of California at Los Angeles
DOI
09:20
5m
Talk
Termination Analysis without the Tears
PLDI
Shaowei Zhu Princeton University, Zachary Kincaid Princeton University
DOI
09:25
5m
Talk
Reverse Engineering for Reduction Parallelization via Semiring Polynomials
PLDI
Akimasa Morihata University of Tokyo, Shigeyuki Sato University of Tokyo
DOI
09:30
5m
Talk
RbSyn: Type- and Effect-Guided Program Synthesis
PLDI
Sankha Narayan Guria University of Maryland, Jeffrey S. Foster Tufts University, David Van Horn University of Maryland
DOI
09:35
5m
Talk
Central Moment Analysis for Cost Accumulators in Probabilistic Programs
PLDI
Di Wang Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Thomas Reps University of Wisconsin
DOI
21:00 - 21:40
Talks 3A: Analysis and SynthesisPLDI at PLDI-A
21:00
5m
Talk
Trace-Based Control-Flow Analysis
PLDI
DOI
21:05
5m
Talk
Demanded Abstract Interpretation
PLDI
Benno Stein University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon, Manu Sridharan University of California at Riverside
DOI
21:10
5m
Talk
Unleashing the Hidden Power of Compiler Optimization on Binary Code Difference: An Empirical Study
PLDI
Xiaolei Ren University of Texas at Arlington, Michael Ho University of Texas at Arlington, Jiang Ming University of Texas at Arlington, Jeff Yu Lei University of Texas at Arlington, Li Li Monash University
DOI
21:15
5m
Talk
Chianina: An Evolving Graph System for Flow- and Context-Sensitive Analyses of Million Lines of C Code
PLDI
Zhiqiang Zuo Nanjing University, Yiyu Zhang Nanjing University, Qiuhong Pan Nanjing University, Shenming Lu Nanjing University, Yue Li Nanjing University, Linzhang Wang Nanjing University, Xuandong Li Nanjing University, Guoqing Harry Xu University of California at Los Angeles
DOI
21:20
5m
Talk
Termination Analysis without the Tears
PLDI
Shaowei Zhu Princeton University, Zachary Kincaid Princeton University
DOI
21:25
5m
Talk
Reverse Engineering for Reduction Parallelization via Semiring Polynomials
PLDI
Akimasa Morihata University of Tokyo, Shigeyuki Sato University of Tokyo
DOI
21:30
5m
Talk
RbSyn: Type- and Effect-Guided Program Synthesis
PLDI
Sankha Narayan Guria University of Maryland, Jeffrey S. Foster Tufts University, David Van Horn University of Maryland
DOI
21:35
5m
Talk
Central Moment Analysis for Cost Accumulators in Probabilistic Programs
PLDI
Di Wang Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Thomas Reps University of Wisconsin
DOI