Stefan Schulze Frielinghaus, Michael Petter and Helmut Seidl. Inter-procedural Two-Variable Herbrand Equalities. Programming Languages and Systems, volume 9032 of Lecture Notes in Computer Science, pages 457-482, 2015. Springer.

We prove that all valid Herbrand equalities can be inter-procedurally inferred for programs where all assignments are taken into account whose right-hand sides depend on at most one variable. The analysis is based on procedure summaries representing the weakest pre-conditions for finitely many generic post-conditions with template variables. In order to arrive at effective representations for all occurring weakest pre-conditions, we show for almost all values possibly computed at run-time, that they can be uniquely factorized into tree patterns and a terminating ground term. Moreover, we introduce an approximate notion of subsumption which is effectively decidable and ensures that finite conjunctions of equalities may not grow infinitely. Based on these technical results, we realize an effective fixpoint iteration to infer all inter-procedurally valid Herbrand equalities for these programs.

Download: PDF Reference: Bibtex The original publication is available at