Interprocedural polynomial invariants

This thesis describes techniques for static analysis of polynomial equalities in interprocedural programs. It elaborates on approaches for analysing polynomial equalities over different domains as well as techniques to apply polynomial analysis to infer interprocedurally valid equalities of uninterpreted terms. This work is organised in three major theoretical parts, followed by a part on practical issues of interprocedural program analysis. In the first part forward and backward frameworks for inferring polynomial equalities are presented to deal with procedure calls. It is shown how to make use of polynomial ideals as abstraction of program states. In the second part, values of variables are treated as integers modulo a power of 2 which coincides with the treatment of integers in most current architectures. The third part is dedicated to interprocedurally infer Herbrand equalities. This gives rise to a novel subclass of the general problem which can be analysed precisely.