[TYPES/announce] PERR 2019 CFP (extended) -- 3rd Workshop on Program Equivalence and Relational Reasoning

[Nikos Tzevelekos]

[with apologies for cross-postings]

======================================================================

                                PERR 2019
       3rd Workshop on Program Equivalence and Relational Reasoning

    A workshop at ETAPS 2019 in Prague
    (European Joint Conferences of Theory & Practice of Software)

======================================================================

Important dates:
    Submission deadline      Fri 8 Feb 2019 (extended)
    Notification             Fri 1 Mar 2019
    Workshop                 Sat 6 Apr 2019


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.


Topics

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 (but are not limited to):

    .    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.

    https://easychair.org/conferences/?conf=perr19

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.


Program Committee

Stefan Ciobaca, Alexandru Ioan Cuza University of Iasi
Steve Kremer, INRIA
Shuvendu K. Lahiri, Microsoft Research
Xavier Leroy, Collège de France
Andrzej Murawski, University of Oxford
Philipp Ruemmer, Uppsala University
Rahul Sharma, Microsoft Research
Ofer Strichman, Technion
Nikos Tzevelekos, Queen Mary University of London
Mattias Ulbrich, Karlsruhe Institute of Technology
Niels Voorneveld, University of Ljubljana