Hi everyone,
I will be giving a
practice
talk for pldi this Friday, May 19, at 3pm in CS 4310. If you are able to attend, I would very much value your feedback.
Title: Automatic Program Inversion using Symbolic Transducers
Abstract: 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.
Best,
Qinheping Hu
![[Computer Systems Lab]](http://www.cs.wisc.edu/pics/csl_logo.gif){kind=logo}