SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Sat 10 Dec 2022 16:30 - 17:00 at Lecture Theatre 2 - Synthesis III Chair(s): Ilya Sergey

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 way $\mathtt{yacc}$ automates the construction of parsers. Our method treats the problem as a program-synthesis problem. The user provides specifications of (i) the concrete semantics of a given operation $\textit{op}$, (ii) the abstract domain $A$ to be used by the analyzer, and (iii) the semantics of a domain-specific language $L$ in which the abstract transformer is to be expressed. As output, our method creates an abstract transformer for $\textit{op}$ in abstract domain $A$, expressed in $L$ (an “$L$-transformer for $\textit{op}$ over $A$”). Moreover, the abstract transformer obtained is a most-precise $L$-transformer for $\textit{op}$ over $A$; that is, there is no other $L$-transformer for $\textit{op}$ over $A$ that is strictly more precise.

We implemented our method in a tool called AMURTH. We used AMURTH to create sets of replacement abstract transformers for those used in two existing analyzers, and obtained essentially identical performance. However, when we compared the existing transformers with the transformers obtained using AMURTH, we discovered that four of the existing transformers were unsound, which demonstrates the risk of using manually created transformers.

Sat 10 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:00
Synthesis IIIOOPSLA at Lecture Theatre 2
Chair(s): Ilya Sergey National University of Singapore
15:30
30m
Research paper
Automated transpilation of imperative to functional code using neural-guided program synthesis
OOPSLA
Benjamin Mariano University of Texas at Austin, Yanju Chen University of California at Santa Barbara, Yu Feng University of California at Santa Barbara, Greg Durrett University of Texas at Austin, Işıl Dillig University of Texas at Austin
DOI
16:00
30m
Talk
Synthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
OOPSLA
Yanju Chen University of California at Santa Barbara, Yuepeng Wang Simon Fraser University, Maruth Goyal University of Texas at Austin, James Dong Stanford University, Yu Feng University of California at Santa Barbara, Işıl Dillig University of Texas at Austin
DOI
16:30
30m
Talk
Synthesizing Abstract Transformers
OOPSLA
Pankaj Kumar Kalita IIT Kanpur, Sujit Kumar Muduli IIT Kanpur, Loris D'Antoni University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Subhajit Roy IIT Kanpur
DOI