Moments in Time: Algebraic Analysis for Solvable Loops (Invited Talk)

Abstract

With substantial progress in automated reasoning, algebraic approaches emerged to automatically analyse program loops in an exact manner. In this invited talk, we discuss recent results in characterizing the functional behaviour of loops with polynomial arithmetic and probabilistic updates. This problem remains unsolved even when we restrict consideration to loops that are non-nested, without conditionals, and/or without exit conditions [Ehud Hrushovski et al., 2023; Julian Müllner and others, 2024]. 
We are motivated by applications of computer-aided verification, in particular to assess the safety, security, and sensitivity of computer systems [M. Z. Kwiatkowska et al., 2011; Gilles Barthe et al., 2012; Gilles Barthe and others, 2018; Marcel Moosbrugger et al., 2023; Alessandro Abate et al., 2023; Andrey Kofnov and others, 2024]. We are interested in modeling, deciding, and solving loop analysis. The key to our work are moment-computable loops [L. Kovács, 2008; Marcel Moosbrugger et al., 2022] which allow us to set limits on what is decidable and solvable in loop analysis. Our approach combines algebra, statistics, and automated reasoning to mechanize loop analysis. Various techniques, such as martingale theory and quantifier elimination, can be seen as examples of moment-computable loop analysis. 
This talk is structured within three inter-connected parts. We first bring moment-based loop analysis into the landscape of {loop invariant synthesis} and extend moment-computable loops with {termination guarantees}. We next automate the reasoning about (probabilistic) loops by summarizing loop semantics as (probabilistic) algebraic recurrences, whose closed-form solutions capture (higher-order) moments, and hence invariants, among loop variables. These recurrences together with loop tests yield moment-based (super)martingales necessary to prove loop termination and compute probability bounds on termination. We finally describe moment-computable loops whose invariant synthesis {decidable} or as {hard} as open problems, such as the Skolem problem [Graham Everest et al., 2003; Terrence Tao, 2008].