Project Seminar Formal Methods in Computer Science (WS 2007/08)

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.

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

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.