Program Equivalence

Motivation

Program equivalence is arguably one of the most interesting and at the same time important problems in formal verification. It has attracted the interest of several communities, ranging from the field of denotational semantics and the problem of full abstraction, compiler verification, to software verification and regression testing {research areas with little overlap in their conferences.

The aim of this Dagstuhl Seminar is to bring together the key players of the different research fields addressing program equivalence with the goal to facilitate the cross-pollination of research between these areas and to help initiate international collaborative research.

There will be plenty of opportunities for participants to present and discuss their own work as well as engaging in discussions. It is a goal of the seminar that this exchange of ideas will lead to the identification of new, discipline-spanning research questions and directions in program equivalence. One challenge that will be addressed in the seminar is to identify and describe concepts for a common formal background which allow the different formal equivalence approaches to be integrated.

Representatives of the following research areas that have addressed program equivalence will meet and exchange ideas at the seminar:

• Regression verification – A particular branch of the program equivalence problem that focuses on proving the equivalence of successive, closely related versions of a program. It has the potential of being easier in practice than applying functional verification to the newer version against a user-defined, high-level specification. There are two reasons for this claim. First, it mostly circumvents the problem of specifying what the program should do. The user can take a no-action default specification by which the outputs of the program should remain unchanged if the two programs are run with the same inputs. Second, there are various opportunities for abstraction and decomposition that are only relevant to the problem of proving equivalence between similar programs. There is a need for methods and tools that can aid the developers understand the impact of changes faster. One may think about such tools assemantic-differencing".
• Semantics – The semantics approach to program equivalence attempts to devise fully abstract models of programs in some appropriate theory, which typically combines operational and denotational paradigms. There are two central themes here: The first one looks at proof techniques stemming from logical relations and open bisimulations, and combinations thereof. Logical relations are type-based approaches which establish equivalence in an inductive fashion, while open bisimulations (often called environmental bisimulations), establish equivalence in a co-inductive operational manner. A different set of techniques has been developed for automated model checking of equivalence. These are based on game semantics, a theory that models open code through formal interactions in the form of 2-player games. Checking equivalence is then reduced to equivalence checking in appropriately crafted abstract machines. Thus, the approach combines denotational models with techniques for automata-based verification, to construct fully automated equivalence routines.
• Translation validation – a formal verification technique, by which the target code of a compiler / translator is proved to be semantically equivalent to the source code. Why verify the translation each time instead of the translator, once? First, a compiler is a very complex software, and generally compiler validation is a daunting task. Second, even if the compiler can be proven to be correct, the proof is immediately invalidated once there is a change in the compiler's code. On the other hand verifying the translation, although still generally undecidable, is more robust to compiler changes, because the languages themselves change less frequently than the compiler. Translation validation was used in the past for verifying synchronous-to-sequential code translation, verifying various optimization steps of GCC, verifying compilation to binary, and for cross-version compiler validation. >Other relational problems – Although not directly an instance of program equivalence, other relational problems like non-interference and secure information flow are closely related to it. Like program equivalence they compare two program instances. Non-interference does not compare two different programs, but two executions of the same program with different secret data. Since information flow is also concerned with (partial) equality in the output state, similar verification techniques using coupling predicates and mutual summaries can be used to successfully discharge proof obligations of both problems.

This seminar will provide a unique opportunity to serve as a nucleus for a new active interdisciplinary research community around the diverse topic of program equivalence.