This paper presents a new approach for synthesizing missing parts from imperative programs by using abstract interpretation and logical abduction. Given a partial program with missing arbitrary expressions, our approach synthesizes concrete expressions that are strong enough to prove the assertions in the given program. Furthermore, the synthesized elements by our approach are the simplest and the weakest among all possible that guarantee the validity of assertions. In particular, we use a combination of forward and backward numerical analyses based on abstract interpretation to generate constraints that are solved by using the logical abduction technique.

We have implemented our approach in a prototype synthesis tool for C programs, and we show that the proposed approach is able to successfully synthesize arithmetic and boolean expressions for various C programs.