Algebraic Analysis of Loop Programs

Abstract

Automated reasoning about programs motivates the problems discussed in this thesis. In the area of formal verification, rigorous mathematical methods are employed to infer properties of programs and, in particular, prove their correctness. Program correctness is defined with respect to a specification that relates the inputs of the program to the outputs it should return. Partial correctness requires that if an output is returned, it will be correct, and is thus different from total correctness, which additionally requires that the algorithm terminates, i.e., eventually reaches a certain state and returns an output. Reasoning about both partial and total correctness of programs is particularly challenging in the presence of recursive components, such as unbounded loops. Loop invariants are assertions that hold before and after each iteration of the loop. A loop invariant can be viewed as an abstract specification that captures the essential effect of the loop, and with that, helps to prove partial correctness. Automatically generating invariants is the crux of correctness reasoning, and complete methods often require algebraic techniques.From the perspective of termination analysis, reasoning about the finiteness of executions is at least as challenging. Already for loops with several linear updates and zero tests, termination problems become undecidable.The hardness of the problems we study justifies considering syntactically restricted classes of loops. Keyto our approach is to model programs as abstract transition systems with associated variables that are subject to polynomial updates. In this thesis, we consider various refinements of such programs, and we relate them to other computation models and their respective enigmas. Oftentimes, our goal is to outline the boundary of (un-)decidability for different classes of programs and loops. To this end, we present both positive and negative results on termination of certain classes of loops. Moreover, we study the invariants from an algebro-geometric perspective and identify notions of invariants most suitable for the respective classes of loops.We also investigate the computational complexity of generating the strongest invariants in several abstract domains.In the later part of this work, we focus on program synthesis, whose aim is to construct a program that satisfies a desired specification. We study loop synthesis, and the natural choice for specifications in this setting are loop invariants. In this thesis, our goal is to synthesise simple loops that satisfy the given invariants.The invariants we consider are algebraic, that is, defined by polynomial equalities among the variables. Thus, we also contribute to the characterisation of algebraic invariants that loops may exhibit.Throughout the chapters of this thesis, we primarily use algebraic methods to reason rigorously about program loops. These methods include, but are not limited to, linear algebra, topology, algebraic geometry, and number theory.