Stefan Schulze Frielinghaus ; Michael Petter ; Helmut Seidl - Inter-procedural Two-Variable Herbrand Equalities

lmcs:3655 - Logical Methods in Computer Science, May 12, 2017, Volume 13, Issue 2 - https://doi.org/10.23638/LMCS-13(2:5)2017
Inter-procedural Two-Variable Herbrand EqualitiesArticle

Authors: Stefan Schulze Frielinghaus ; Michael Petter ; Helmut Seidl

    We prove that all valid Herbrand equalities can be inter-procedurally inferred for programs where all assignments whose right-hand sides depend on at most one variable are taken into account. 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 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. Finally we show that an invariant candidate with a constant number of variables, can be verified in polynomial time.


    Volume: Volume 13, Issue 2
    Published on: May 12, 2017
    Accepted on: May 12, 2017
    Submitted on: May 12, 2017
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1330 times.
    This article's PDF has been downloaded 336 times.