(Un)Solvable Loop Analysis

10^th October 2023, 13:00 Ashton Lecture Theatre
Dr. George Kenison
School of Computer Science and Mathematics, Liverpool John Moores University

Abstract

Loop invariants are program properties that hold both before and after every loop iteration. On the one hand, automatically synthesising polynomial loop invariants in the restricted setting of single-path loops with linear updates is computable. On the other hand, synthesising polynomial invariants for loops with polynomial updates (so called polynomial loops) is an open problem.

In this talk we review established algebraic techniques for automatically computing polynomial invariants for a class of single-path polynomial loops (so called solvable loops). We will then demonstrate a new technique for synthesising invariants for polynomial loops that are not solvable (so called unsolvable loops).

This is joint work with: Daneshvar Amrollahi, Ezio Bartocci, Laura Kovács, Marcel Moosbrugger, and Miroslav Stankovič.