Synthesis to repair heap-manipulating programs using Java StarFinder

The state of art of program repair for heap manipulating program has focus on specific properties of bugs, like null pointer dereference. We try to fix programs with pre-condition and post-condition written in separation logic. Given a program, we first run JSF to collect its post-state(p) by symbolic execution with the given pre-condition. Then we check if p entails the given post-condition(p'). If not, a bug is detected. Our approach to program repair has two main components: abduction and repair specification inference. First, we propose to infer the missing information to establish the post-condition through abduction using an existing solver. In particular, we infer a constraint f such that p * f is satisfied and p * f |-> p'. Secondly, based on abduction, we symbolically execute the input program with the abduction in a backward manner in order to construct repair specifications at every line of the input program. These repair specifications help to infer valid Hoare-style triples with fix candidates.