06105897

a

06105897 Cachera, David Jensen, Thomas Jobin, Arnaud Kirchner, Florent Inference of polynomial invariants for imperative programs: a farewell to Gr\"obner bases. Min\'e, Antoine (ed.) et al., Static analysis. 19th international symposium, SAS 2012, Deauville, France, September 11--13, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33124-4/pbk). Lecture Notes in Computer Science 7460, 58-74 (2012). 2012 Berlin: Springer EN

doi:10.1007/978-3-642-33125-1_7

Summary: We propose a static analysis for computing polynomial invariants for imperative programs. The analysis is derived from an abstract interpretation of a backwards semantics, and computes pre-conditions for equalities like $g = 0$ to hold at the end of execution. A distinguishing feature of the technique is that it computes polynomial loop invariants without resorting to Gr\"obner base computations. The analysis uses remainder computations over parameterized polynomials in order to handle conditionals and loops efficiently. The algorithm can analyse and find a large majority of loop invariants reported previously in the literature, and executes significantly faster than implementations using Gr\"obner bases.