In the rest of this paper, we first motivate our results on examples for invariant and loop synthesis
(Section ). We then
report on
algebra-based approaches for invariant generation
(Section ) and loop synthesis
(Section ), by summarising our main
results published at [1]}, [2]}.
