The techniques in [1]}, [2]}, [3]}, [4]}
approximate an arbitrary loop by a single-path loop and then apply recurrence
solving to infer nonlinear invariants. They include guards in loops and
conditionals in their reasoning, and are also able to infer
inequalities as loop invariant.
A data-driven approach to invariant generation is given
in [5]} using the guess-and-check methodology. Linear
algebra is used to guess candidate invariants from data generated by concrete
program executions where an upper bound on the polynomial degree of the
candidate is user-given. An SMT solver is then used to validate the candidates
with respect to the properties of loop invariants. If this is not the case, then
the candidate is refined based on the output of the SMT solver.
