Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 Virtual Conference

This program is tentative and subject to change.

Thu 24 Jun 2021 13:35 - 13:40 at PLDI-A - Talks 4A: Analysis and Synthesis
Fri 25 Jun 2021 01:35 - 01:40 at PLDI-A - Talks 4A: Analysis and Synthesis

Implementations of many data structures use several correlated fields to improve their performance; however, inconsistencies between these fields can be a source of serious program errors. To address this problem, we propose a new technique for automatically refining data structures from integrity constraints. In particular, consider a data structure $D$ with fields $F$ and methods $M$, as well as a new set of auxiliary fields $F'$ that should be added to $D$. Given this input and an integrity constraint $\Phi$ relating $F$ and $F'$, our method automatically generates a refinement of $D$ that satisfies the provided integrity constraint. Our method is based on a \emph{modular} instantiation of the CEGIS paradigm and uses a novel inductive synthesizer that augments top-down search with three key ideas. First, it computes \emph{necessary preconditions} of partial programs to dramatically prune its search space. Second, it augments the grammar with promising new productions by leveraging the computed preconditions. Third, it guides top-down search using a \emph{probabilistic} context-free grammar obtained by statically analyzing the integrity checking function and the original code base. We evaluated our method on 25 data structures from popular Java projects and show that our method can successfully refine 23 of them. We also compare our method against two state-of-the-art synthesis tools and perform an ablation study to justify our design choices. Our evaluation shows that (1) our method is successful at refining many data structure implementations in the wild, (2) it advances the state-of-the-art in synthesis, and (3) our proposed ideas are crucial for making this technique practical.

This program is tentative and subject to change.

Conference Day
Thu 24 Jun

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

13:30 - 14:05
Talks 4A: Analysis and SynthesisPLDI at PLDI-A +12h
13:30
5m
Talk
Phased Synthesis of Divide and Conquer Programs
PLDI
Azadeh FarzanUniversity of Toronto, Victor NicoletUniversity of Toronto
DOI
13:35
5m
Talk
Synthesizing Data Structure Refinements from Integrity Constraints
PLDI
Shankara PailoorUniversity of Texas at Austin, Yuepeng WangUniversity of Pennsylvania, Xinyu WangUniversity of Michigan, Isil DilligUniversity of Texas at Austin
DOI
13:40
5m
Talk
Cyclic Program Synthesis
PLDI
Shachar ItzhakyTechnion, Hila PelegUniversity of California at San Diego, Nadia PolikarpovaUniversity of California at San Diego, Reuben N. S. RoweRoyal Holloway University of London, Ilya SergeyYale-NUS College; National University of Singapore
DOI
13:45
5m
Talk
Adaptive Restarts for Stochastic Synthesis
PLDI
Jason R. KoenigStanford University, Oded PadonVMware Research; Stanford University, Alex AikenStanford University, USA
DOI
13:50
5m
Talk
JPortal: Precise and Efficient Control-Flow Tracing for JVM Programs with Intel Processor Trace
PLDI
Zhiqiang ZuoNanjing University, Kai JiNanjing University, Yifei WangNanjing University, Wei TaoNanjing University, Linzhang WangNanjing University, Xuandong LiNanjing University, Guoqing Harry XuUniversity of California at Los Angeles
DOI
13:55
5m
Talk
IOOpt: Automatic Derivation of I/O Complexity Bounds for Affine Programs
PLDI
Auguste OlivryInria, Guillaume IoossInria, Nicolas TollenaereInria, Atanas RountevOhio State University, Saday SadayappanUniversity of Utah, Fabrice RastelloInria
DOI
14:00
5m
Talk
Proving Non-termination by Program Reversal
PLDI
Krishnendu ChatterjeeIST Austria, Ehsan Kafshdar GoharshadyFerdowsi University of Mashhad, Petr NovotnýMasaryk University, Đorđe ŽikelićIST Austria
DOI

Conference Day
Fri 25 Jun

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

01:30 - 02:05
Talks 4A: Analysis and SynthesisPLDI at PLDI-A
01:30
5m
Talk
Phased Synthesis of Divide and Conquer Programs
PLDI
Azadeh FarzanUniversity of Toronto, Victor NicoletUniversity of Toronto
DOI
01:35
5m
Talk
Synthesizing Data Structure Refinements from Integrity Constraints
PLDI
Shankara PailoorUniversity of Texas at Austin, Yuepeng WangUniversity of Pennsylvania, Xinyu WangUniversity of Michigan, Isil DilligUniversity of Texas at Austin
DOI
01:40
5m
Talk
Cyclic Program Synthesis
PLDI
Shachar ItzhakyTechnion, Hila PelegUniversity of California at San Diego, Nadia PolikarpovaUniversity of California at San Diego, Reuben N. S. RoweRoyal Holloway University of London, Ilya SergeyYale-NUS College; National University of Singapore
DOI
01:45
5m
Talk
Adaptive Restarts for Stochastic Synthesis
PLDI
Jason R. KoenigStanford University, Oded PadonVMware Research; Stanford University, Alex AikenStanford University, USA
DOI
01:50
5m
Talk
JPortal: Precise and Efficient Control-Flow Tracing for JVM Programs with Intel Processor Trace
PLDI
Zhiqiang ZuoNanjing University, Kai JiNanjing University, Yifei WangNanjing University, Wei TaoNanjing University, Linzhang WangNanjing University, Xuandong LiNanjing University, Guoqing Harry XuUniversity of California at Los Angeles
DOI
01:55
5m
Talk
IOOpt: Automatic Derivation of I/O Complexity Bounds for Affine Programs
PLDI
Auguste OlivryInria, Guillaume IoossInria, Nicolas TollenaereInria, Atanas RountevOhio State University, Saday SadayappanUniversity of Utah, Fabrice RastelloInria
DOI
02:00
5m
Talk
Proving Non-termination by Program Reversal
PLDI
Krishnendu ChatterjeeIST Austria, Ehsan Kafshdar GoharshadyFerdowsi University of Mashhad, Petr NovotnýMasaryk University, Đorđe ŽikelićIST Austria
DOI