3rd Workshop on Program Equivalence and Relational ReasoningPERR 2019

This workshop is dedicated to the formal verification of program equivalence and related relational problems. It is the 3rd in a series of meetings that bring together researchers from different areas interested in equivalence. The topic touches many aspects of formal methods: regression verification, translation validation, verified compilation, language semantics, deductive verification, (bounded) model checking, specification inference, software evolution and testing.

The goal of the workshop is to bring researchers of the different fields in touch and to stipulate an exchange of ideas leading to forging a community working on PERR. It welcomes contributions from the mentioned topics but is also open to new questions regarding program equivalence. This includes related research areas of relational reasoning like program refinement or the verification of hyper-properties, in particular of secure information flow.

Accepted Papers

Call for Papers

PERR is an annual international workshop dedicated to the formal verification of program equivalence and related relational problems. It is the 3rd in a series of meetings that bring together researchers from different areas interested in equivalence and related questions. PERR 2019 will be held as satellite workshop of ETAPS (http://www.etaps.org/).

Program equivalence is arguably one of the most interesting and at the same time important problems in formal verification. It is a cross-cutting topic that has attracted the interest of several research communities: the field of denotational (game) semantics, deductive software verification, bounded model checking, specification inference, software evolution and regression testing, etc.

The goal of the workshop is to bring researchers of the different fields in touch and to stipulate an exchange of ideas leading to forging a community working on PERR. It welcomes contributions from the topics mentioned above but is also open to new questions regarding program equivalence. This includes related research areas of relational reasoning like program refinement or the verification of hyperproperties, in particular of secure information flow.

Areas of interest include:

• regression verification
• program equivalence
• equivalence of higher order programs
• product programs, relational calculi
• verification of hyperproperties
• program refinement, refinement calculus
• specification of differences between programs
• inferring semantic differences between programs
• transformation validation
• correct compiler transformations
• automata bisimulation
• code equivalence checking in teaching and marking

This is an informal workshop that welcomes work in progress, overviews of more extensive work, programmatic or position papers and tool presentations.

The workshop will have informal proceedings, posted on its webpage, and speakers will be asked to consider submitting papers towards a post-proceedings volume.

Submission Instructions

Please submit an abstract (this can be in the form of 1-2 pages of text, or a paper of no more than 15 pages) of your proposed talk on the EasyChair submission page below. Submissions will be reviewed by at least 2 PC members and feedback will be provided.

The workshop will have informal proceedings, posted on its webpage, and speakers will be asked to consider submitting papers towards an EPTCS post-proceedings volume.