Linear Loop Synthesis from Polynomial Invariants
- 16:00 23rd November 2023 ( week 7, Michaelmas Term 2023 )051
A loop invariant is a relation among variables that holds before and after every iteration of a program loop.
Invariants provide inductive arguments that are key for the formal verification of
recursive programs.
Automated generation of reasonable invariants is a much-desired step to
proving program correctness. In quest of understanding what relations
can be invariant for a loop with linear updates, we address the inverse
problem--finding (synthesising) linear loops that satisfy given
invariants. Loops synthesised modulo invariants are correct by design
and no longer need to be verified.
In this line of work, we consider invariants specified by polynomial
equalities. Two classes of such invariants are discussed: a)
conjunctions of pure difference binomials, and b) quadratic equations.
We introduce an algorithmic approach that constructs linear loops from
such polynomial invariants, by generating linear recurrence sequences
that have given algebraic relations amongst their terms. In particular,
we provide a procedure that, given a quadratic equation, decides whether
a loop satisfying this equation exists and, if the answer is positive,
the procedure synthesises a loop and ensures its variables achieve
infinitely many different values.
Speaker Bio
Anton Varonka is a PhD student at the Forsyte group at TU Wien, under
the supervision of Laura Kovács. Anton received his master's degree from
Saarland University, where he was part of Joel Ouaknine's group at
MPI-SWS. Before that, Anton did his undergraduate studies at Belarusian
State University.
Anton's work focuses on the computability aspects of
verification-motivated problems. He is most interested in studying the
expressivity of different models of computation and applying algebraic
techniques.
Share this:
