Yet, both in the setting of verification and synthesis, one of the main
challenges is to verify and/or synthesize loops/recursion. In verification,
solving this challenge requires generating additional program assertions in the
form of loop
invariants [1]}, [2]}, [3]}.
Intuitively, a loop invariant is a formal description of the behavior of the
loop, expressing loop properties that hold before and after each loop iteration.
In synthesis, the challenge of reasoning with loops comes by answering the
question whether there exists a loop satisfying a given loop invariant and
constructively synthesizing a loop with respect to a given invariant. We refer
to this task of synthesis as loop synthesis. Note that loop synthesis can
be considered as the reverse problem of loop invariant generation: rather than
generating invariants summarizing a given loop, we synthesize loops whose
summaries are captured by a given invariant property.
