While-guard Synthesis by Abstract Static Analysis and CHC Solving

This paper introduces a novel technique for automatically synthesizing assertion-safe while-guards in imperative programs.Given a partial program (sketch) with missing whileguards, the proposed algorithm synthesizes complete Boolean expressions for the missing ones, such that the obtained complete program satisfies the given assertions.To solve this problem, our technique uses forward and backward abstract static analyses of programs to generate (logical) constraints with unknown predicates that are subsequently solved by employing the logical Constraint Horn Clause (CHC) solvers.We have implemented our synthesis algorithm in a proofof-concept tool, and evaluated it on a set of C programs with missing while-guards.By experiments we prove the effectiveness of the proposed technique for synthesizing arbitrary Boolean expressions defined over program variables for some interesting program sketches written in C.