Algebra-Based Loop Analysis

Abstract

Automating loop analysis, and in particular synthesizing loop invariants, is a central challenge in the computer-aided verification of programs with loops, with applications in compiler optimization, probabilistic programming and IT security. While this challenge is in general undecidable, several techniques have emerged to automatically summarize the functional behaviour of software loops, thus providing inductive loop invariants that may prevent programmers from introducing errors while making changes in their code. In this tutorial, we show that novel combinations of methods from computer algebra, algorithmic combinatorics and static loop analysis provide powerful workhorses to derive (all) polynomial loop invariants, synthesize affine loops from invariants, and infer quantitative properties over the value distributions of probabilistic loop variables.