English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Loop invariants are software properties that hold before and after everyiteration of a loop. As such, invariants provide inductive arguments that arekey in automating the verification of program loops. The problem of generatingloop invariants; in particular, invariants described by polynomial relations(so called polynomial invariants), is therefore one of the hardest problems insoftware verification. In this paper we advocate an alternative solution toinvariant generation. Rather than inferring invariants from loops, wesynthesise loops from invariants. As such, we generate loops that satisfy agiven set of polynomials; in other words, our synthesised loops are correct byconstruction.  Our work turns the problem of loop synthesis into a symbolic computationchallenge. We employ techniques from algebraic geometry to synthesise loopswhose polynomial invariants are described by pure difference binomials. We showthat such complex polynomial invariants need ``only'' linear loops, opening upnew venues in program optimisation. We prove the existence of non-trivial loopswith linear updates for polynomial invariants generated by pure differencebinomials. Importantly, we introduce an algorithmic approach that constructslinear loops from such polynomial invariants, by generating linear recurrencesequences that have specified algebraic relations among their terms.

From Polynomial Invariants to Linear Loops