  Provably correct software is one of the key challenges in our softwaredriven
society. While formal verification establishes the correctness of a given
program, the result of program synthesis is a program which is correct by
construction. In this paper we overview some of our results for both of these
scenarios when analysing programs with loops. The class of loops we consider
can be modelled by a system of linear recurrence equations with constant
coefficients, called C-finite recurrences. We first describe an algorithmic
approach for synthesising all polynomial equality invariants of such
non-deterministic numeric single-path loops. By reverse engineering invariant
synthesis, we then describe an automated method for synthesising program loops
satisfying a given set of polynomial loop invariants. Our results have
applications towards proving partial correctness of programs, compiler
optimisation and generating number sequences from algebraic relations.
  This is a preprint that was invited for publication at VMCAI 2021.
