Inter-procedural Two-Variable Herbrand Equalities

We prove that all valid Herbrand equalities can be inter-procedurallyinferred for programs where all assignments whose right-hand sides depend on atmost one variable are taken into account. The analysis is based on proceduresummaries representing the weakest pre-conditions for finitely many genericpost-conditions with template variables. In order to arrive at effectiverepresentations for all occurring weakest pre-conditions, we show for almostall values possibly computed at run-time, that they can be uniquely factorizedinto tree patterns and a ground term. Moreover, we introduce an approximatenotion of subsumption which is effectively decidable and ensures that finiteconjunctions of equalities may not grow infinitely. Based on these technicalresults, we realize an effective fixpoint iteration to infer allinter-procedurally valid Herbrand equalities for these programs. Finally weshow that an invariant candidate with a constant number of variables, can beverified in polynomial time