Sponsored by:

Association for Computing Machinery - SIGSAM

Tutorial Speakers

Titles and Abstracts

Paola Boito
UniversitĂ  di Pisa, Italy




Irina Kogan
North Carolina State University, USA

Invariants: Computation and Applications

Abstract: Invariants withstand transformations and, therefore, represent the essence of objects or phenomena. In mathematics, transformations often constitute a group action. Since the 19th century, studying the structure of various types of invariants and designing methods and algorithms to compute them remain an active area of ongoing research with an abundance of applications. In this incredibly vast topic, we focus on two particular themes displaying a fruitful interplay between the differential and algebraic invariant theories. First, we show how an algebraic adaptation of the moving frame method from differential geometry leads to a practical algorithm for computing a generating set of rational invariants. Then we discuss the notion of differential invariant signature, its role in solving equivalence problems in geometry and algebra, and some successes and challenges in designing algorithms based on this notion. Our goal is to convey the core ideas in a self-contained, accessible, and practical manner, often through examples, sometimes at an expense of complete rigor and generality, while providing references to more comprehensive treatments of the subject.

Laura Kovács
TU Wien, Austria

Algebra-Based Loop Analysis

Abstract: Automating loop analysis, and in particular synthesizing loop invariant, 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.

The key ingredients of our work root in (i) static analysis, to model loops as algebraic recurrence equations over the loop counter and to impose structural constraints over loops in order to guarantee that the resulting recurrences equations can be reduced to linear recurrences with constant coefficients; (ii) in symbolic summation and polynomial algebra, to solve recurrences and eliminate loop counters/recurrence variables by applying Groebner basis computation over closed-forms; (iii) in applied statistics, to compute quantitative loop invariants over higher-order statistical moments of polynomial probabilistic loops, and (iv) in automated reasoning, to simplify loop constraints and to use invariants towards ensuring functional correctness of loops.