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.