Section outline

    Proving Program Equivalence in Translation Validation
    Andrei Voronkov (University of Manchester)
    (Joint work with Iman Narasamdya)

    Hagenberg Seminar Room, 13:00-14:00

    The problem of translation validation in optimising compilers can be
    formulated as follows. Given two programs P1 and P2 such that P2 is
    obtained from P1 by applying some transformation (for example, performed
    by an optimising compiler), prove automatically that P2 and P1 are
    equivalent.

    The problem may turn out to be simpler than the general problem of
    program equivalence since P1 and P2 may be similar to each other and
    this similarity can be exploited in addition to properties of P1
    and P2.


    We propose an approach for proving program equivalence based on
    inter-program invariants: a generalisation of program invariants for the
    case of two programs. To this end, we first present the standard theory
    of invariants in an abstract form and then develop a similar theory for
    the case of two programs.