POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Thu 18 Jan 2024 09:00 - 09:20 at Kelvin Lecture - Synthesis 2 Chair(s): Michael Hicks

Modifications to the data representation of an abstract data type (ADT) can require significant semantic refactoring of the code. Motivated by this observation, this paper presents a new method to automate semantic code refactoring tasks. Our method takes as input the original ADT implementation, a new data representation, and a so-called \emph{relational representation invariant} (relating the old and new data representations), and automatically generates a new ADT implementation that is semantically equivalent to the original version. Our method is based on counterexample-guided inductive synthesis (CEGIS) but leverages three key ideas that allow it to handle real-world refactoring tasks. First, our approach reduces the underlying relational synthesis problem to a set of (simpler) programming-by-example problems, one for each method in the ADT. Second, it leverages symbolic reasoning techniques, based on logical abduction, to deduce code snippets that should occur in the refactored version. Finally, it utilizes a notion of \emph{partial equivalence} to make inductive synthesis much more effective in this setting. We have implemented the proposed approach in a new tool called Revamp for automatically refactoring Java classes and evaluated it on 30 Java class mined from Github. Our evaluation shows that Revamp can correctly refactor the entire ADT in 97% of the cases and that it can successfully re-implement 144 out of the 146 methods that require modifications.

Thu 18 Jan

Displayed time zone: London change

09:00 - 10:20
Synthesis 2POPL at Kelvin Lecture
Chair(s): Michael Hicks Amazon Web Services and the University of Maryland
09:00
20m
Talk
Semantic Code Refactoring for Abstract Data Types
POPL
Shankara Pailoor University of Texas at Austin, Yuepeng Wang Simon Fraser University, Işıl Dillig University of Texas at Austin
09:20
20m
Talk
API-driven Program Synthesis for Testing Static Typing Implementations
POPL
Thodoris Sotiropoulos ETH Zurich, Stefanos Chaliasos Imperial College London, Zhendong Su ETH Zurich
09:40
20m
Talk
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
POPL
Kevin Batz RWTH Aachen University, Tom Biskup RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University
10:00
20m
Talk
A Case for Synthesis of Recursive Quantum Unitary Programs
POPL
Haowei Deng University of Maryland at College Park, Runzhou Tao Columbia University, Yuxiang Peng University of Maryland, Xiaodi Wu University of Maryland