Search

Loop invariant generation, which automates the generation of assertions that always hold inside loops, has many important applications such as safety analysis, reachability analysis and complexity-bound analysis. However, automated invariant generation for arbitrary loops is an undecidable problem. In this paper, we target at an important category of loops, namely affine loops, which widely exist in many programs but still lack general approach to invariant generation. We, however, provide a sound and complete approach based on matrix algebra to automatically synthesizing inductive invariants in the form of an affine inequality. Specifically, for the situation when the loop guard is tautological (i.e., 'true'), we show that the eigenvalues and their eigenvectors generate all meaningful affine inductive invariants. Moreover, when the loop guard consists of one or more affine inequalities, we solve the invariant generation problem by (i) first establishing through matrix inverse the relationship between the invariants and a key parameter in the application of Farkas' Lemma, then (ii) solving the feasible domain of the key parameter, and finally (iii) showing that the key parameter can be addressed by a finite set of values w.r.t a tightness condition on the constraints for the invariants. Experimental results using existing and new cases show that our approach can generate affine invariants over linear dynamic systems that inherently involve the non-trivial choices (e.g., eigenvalues, boundary points of the feasible domain, etc.) of the key parameter.

International audience

Probabilistic recurrence relations (PRRs) are a standard formalism to analyze the runtime of randomized algorithms. In this work, we consider the classical problem of obtaining concentration bounds on the runtime of randomized algorithms modeled as PRRs. More specifically, given a time limit k, we study the probability Pr[ T ≥ k ] that the runtime of the algorithm reaches or exceeds the time limit. The key research question in concentration bound analysis is to find an upper-bound function upper(n) ≥ Pr[ T ≥ k ] such that upper(n) converges rapidly to zero as n tends to infinity. The classical approach to this problem is the "cookbook" method by Karp (J. ACM 1994). For the past three decades, finding an approach to improve Karp's classical bounds has been a major open problem. In this work, we first demonstrate a method to obtain such upper-bound functions from a special family of supermartingale functions through the well-known Optional Stopping Theorem (OST). We then provide automated algorithmic approaches to synthesize such supermartingale functions in exponential and polynomial form. Our algorithms are based on the Taylor expansion and tight approximations of the expectation of moments that involve logarithmic terms. Compared with Karp's method, our algorithmic approaches find significantly tighter concentration bounds for several classical randomized algorithms. Moreover, our algorithmic approaches can also find concentration bounds for several randomized algorithms in computational geometry which adopt techniques such as randomized incremental construction. To the best of our knowledge, no previous method was applicable in these cases. Finally, we present experimental results demonstrating the practical versatility and efficiency of our approach..