We propose a new automatic program inversion method for imperative programs that contain loops. In particular, given a loop that produces an output state given a particular input state, our method can synthesize an inverse loop that reconstructs the input state given the original loop's output state. The synthesis process consists of two major components: (a) building the inverse loop's body, and (b) building the inverse loop's predicate. Our method works for all natural loops, including those that take early exits (e.g., via breaks, gotos, returns). This work extends a program analysis and synthesis framework, called Backstroke, that we developed in prior work. © 2013 Springer-Verlag Berlin Heidelberg.
Hou, C., Quinlan, D., Jefferson, D., Fujimoto, R., & Vuduc, R. (2013). Synthesizing loops for program inversion. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7581 LNCS, pp. 72–84). Springer Verlag. https://doi.org/10.1007/978-3-642-36315-3_6