Write a Blog >>
Tue 20 Jun 2017 11:15 - 11:40 at Aula Master - Static Analysis and Security Chair(s): Mayur Naik

We propose a fully-automated technique for inverting functional programs that operate over lists such as string encoders and decoders. We consider programs that can be modeled using symbolic extended finite transducers (\SEFTs), an expressive model that can describe complex list-manipulating programs while retaining several decidable properties. Concretely, given a program $P$ expressed as an \SEFT, we propose techniques for: 1) checking whether $P$ is injective and, if that is the case, 2) building an \SEFT $P^{-1}$ describing its inverse. We first show that it is undecidable to check whether an \SEFT is injective and propose an algorithm for checking injectivity for a restricted, but a practical class of \SEFTs. We then propose an algorithm for inverting \SEFTs based on the following idea: if an \SEFT is injective, inverting it amounts to inverting all its individual transitions. We leverage recent advances program synthesis and show that the transition inversion problem can be expressed as an instance of the syntax-guided synthesis framework. Finally, we implement the proposed techniques in a tool called \genic and show that \genic can invert 13 out 14 real complex string encoders and decoders, producing inverse programs that are substantially identical to manually written ones.

Tue 20 Jun
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:50 - 12:30: PLDI Research Papers - Static Analysis and Security at Aula Master
Chair(s): Mayur NaikGeorgia Tech
pldi-2017-papers10:50 - 11:15
Timos AntonopoulosYale University, Paul GazzilloYale University, Michael HicksUniversity of Maryland, College Park, Eric KoskinenYale University, Tachio TerauchiJAIST, Shiyi WeiUniversity of Maryland, College Park
Media Attached
pldi-2017-papers11:15 - 11:40
Qinheping HuUniversity of Wisconsin-Madison, Loris D'AntoniUniversity of Wisconsin–Madison
Media Attached
pldi-2017-papers11:40 - 12:05
Peter OhmannUniversity of Wisconsin - Madison, Alexander L. BrooksUniversity of Wisconsin, Madison, Loris D'AntoniUniversity of Wisconsin–Madison, Ben LiblitUniversity of Wisconsin–Madison
Pre-print Media Attached
pldi-2017-papers12:05 - 12:30
Goran DoychevIMDEA Software Institute, Boris KöpfIMDEA Software Institute, Spain
Media Attached