Path-Based Inductive Synthesis for Program Inversion

In this paper, the authors investigate the problem of semi-automated inversion of imperative programs, which has the potential to make it much easier and less error prone to write programs that naturally pair as inverses, such as insert/delete operations, compressors/ decompressors, and so on. Viewing inversion as a sub-problem of program synthesis, the authors propose a novel synthesis technique called Path-based Inductive Synthesis (PINS) and apply it to inversion. PINS starts from a program P and a template T for its inverse. PINS then iteratively refines the space of template instantiations by exploring paths in the composition of P and T with symbolic execution.