Infer Precise Program Invariant Using Abstract Interpretation with Recurrence Solving

Program invariant is formal description of properties that should hold at certain program location in every valid execution. It is very useful for program analysis and verification. In this paper, we introduce an abstraction interpretation approach for generating program invariant efficiently and precisely. A polynomial interval domain is proposed for representing abstract state and precise loop effect is summarized by recognizing and solving recurrence relations. Our method has implemented and its effectiveness is shown in various kinds of cases. Experiment results show that our approach generates more accurate program invariants quickly.