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 DecDisplayed time zone: Auckland, Wellington change
15:30 - 17:00 | |||
15:30 30mResearch 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 30mTalk | 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 30mTalk | 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 |