Both in the setting of verification and synthesis, one of the main
challenges is to verify or synthesise programs with
loops/recursion. In formal verification,
solving this challenge requires for example synthesising loop invariants
 [1]}, [2]}, [3]}.
Intuitively, a loop invariant is a formal description of the behaviour of the
loop, expressing loop properties that hold at arbitrary loop
iterations. For the purpose of automating formal verification,
synthesising loop invariants that are
inductive is of critical importance, as inductive invariants describe
program properties/safety assertions that hold
before and after each loop iteration.
