Moments in Time: Algebraic Analysis for Solvable Loops

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 [5, 11]. We are motivated by applications of computer-aided verification, in particular to assess the safety, security, and sensitivity of computer systems [8, 3, 2, 9, 1, 6]. We are interested in modeling, deciding, and solving loop analysis. The key to our work are moment-computable loops [7, 10] 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 [4, 12].