Skip to main content

Synthesizing loops for program inversion

Citations of this article
Mendeley users who have this article in their library.
Get full text


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.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free