Section outline

  • General

    Collapse all Expand all
    Time: Wednesday, 12:30-14:00.
    Room: HA 105 (Hagenberg seminar room).
    Start: October 10, 2007.

    In this seminar, we explore current research and systems for specifying and verifying computer programs (specification languages, program verifiers, model checkers, ...). This continues the seminar of the previous semester.
    To take part in the seminar, you have to enrol in the KUSSS system. If you also login in Moodle and register as a course participant, you will receive per email all messages posted in the News forum.

  • 10 October - 16 October

    • Wolfgang Schreiner: Introduction
    • Wolfgang Schreiner: Reasoning about Control Flow Interruptions

  • 24 October - 30 October

    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.