TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 18151

Program Equivalence

( Apr 08 – Apr 13, 2018 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/18151

Organizers

Contact


Schedule

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.

Copyright Shuvendu Lahiri, Andrzej Murawski, Ofer Strichman, and Mattias Ulbrich

Summary

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, to software verification and Regression Testing. The aim of this meeting was to bring together the different approaches and techniques of the current state of the art and to facilitate the cross-pollination of research between these areas.

This interdisciplinary community met once before in the workshop on program equivalence in London (April 2016). There was a general agreement among the participants that a research community around this topic should be established in the form of a workshop and eventually a conference, and that the interest in this topic continuously grows around the world, including a growing interest in the industry. Furthermore, currently there is little overlap in the conferences that some of the key players attend, to the point that many participants were little aware of other participants' work.

We were happy to witness that indeed participants learned greatly from this week, collaborations were established, and cross fertilization between the communities occurred. We hope to meet again in Dagstuhl in the future!

Copyright Shuvendu Lahiri, Andrzej Murawski, Ofer Strichman, and Mattias Ulbrich

Participants
  • Anindya Banerjee (NSF - Alexandria, US) [dblp]
  • Gilles Barthe (IMDEA Software - Madrid, ES) [dblp]
  • Nick Benton (Facebook - London, GB) [dblp]
  • Dirk Beyer (LMU München, DE) [dblp]
  • Soham Chakraborty (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Stefan Ciobaca (University AI. I. Cuza - Iasi, RO) [dblp]
  • Constantin Enea (University Paris-Diderot, FR) [dblp]
  • Grigory Fedyukovich (Princeton University, US) [dblp]
  • Dan R. Ghica (University of Birmingham, GB) [dblp]
  • Arie Gurfinkel (University of Waterloo, CA) [dblp]
  • Guilhem Jaber (ENS - Lyon, FR) [dblp]
  • Vasileios Koutavas (Trinity College Dublin, IE) [dblp]
  • Steve Kremer (INRIA Nancy - Grand Est, FR) [dblp]
  • Shuvendu K. Lahiri (Microsoft Research - Redmond, US) [dblp]
  • James Laird (University of Bath, GB) [dblp]
  • Xavier Leroy (INRIA - Paris, FR) [dblp]
  • Yi Li (University of Toronto, CA) [dblp]
  • Sergey Mechtaev (National University of Singapore, SG) [dblp]
  • Andrzej Murawski (University of Oxford, GB) [dblp]
  • Kedar Namjoshi (Nokia Bell Labs - Murray Hill, US) [dblp]
  • David A. Naumann (Stevens Institute of Technology, US) [dblp]
  • Julia Rubin (University of British Columbia - Vancouver, CA) [dblp]
  • Philipp Rümmer (Uppsala University, SE) [dblp]
  • Neha Rungta (Amazon.com, Inc. - Palo Alto, US) [dblp]
  • Chaked Saydoff (Technion - Haifa, IL)
  • Rahul Sharma (Microsoft Research India - Bangalore, IN) [dblp]
  • Stephen Siegel (University of Delaware - Newark, US)
  • Marcelo Sousa (University of Oxford, GB) [dblp]
  • Ofer Strichman (Technion - Haifa, IL) [dblp]
  • Aaron Tomb (Galois - Portland, US) [dblp]
  • Nikos Tzevelekos (Queen Mary University of London, GB) [dblp]
  • Mattias Ulbrich (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Niels Voorneveld (University of Ljubljana, SI)

Classification
  • semantics / formal methods
  • verification / logic

Keywords
  • Program equivalence
  • Regression-verification
  • Translation validation