ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic

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

Title
Analysis of program differences with numerical abstract interpretation
PERR
Link to publication Pre-print File Attached
Automatic Equivalence Proofs for Programs with Algebraic Data Types
PERR
Local Reasoning for Robust Observational Equivalence
PERR
On Quantitative Comparison of Chemical Reaction Network Models
PERR
Proving Program Equivalence with Constrained Rewriting Induction and Ctrl
PERR
Relational Verification via Invariant-Guided Synchronization
PERR
Semantics-Based Proofs of Equivalence for Functions with Accumulators
PERR
Understanding Counterexamples for Relational Properties with DIbugger
PERR

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.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sat 6 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
09:00
60m
Talk
Invited talk by Margus Veanes
PERR
Margus Veanes Microsoft Research
10:00
30m
Talk
Local Reasoning for Robust Observational Equivalence
PERR
Dan Ghica University of Birmingham, Koko Muroya RIMS, Kyoto University, JP & University of Birmingham, UK, Todd Waugh Ambridge University of Birmingham
16:00 - 18:00
16:00
30m
Talk
Automatic Equivalence Proofs for Programs with Algebraic Data Types
PERR
Moritz Kiefer , Mattias Ulbrich Karlsruhe Institute of Technology
16:30
30m
Talk
Proving Program Equivalence with Constrained Rewriting Induction and Ctrl
PERR
Carsten Fuhs Birkbeck, University of London, Cynthia Kop Radboud University Nijmegen, Naoki Nishida Nagoya University
17:00
30m
Talk
Semantics-Based Proofs of Equivalence for Functions with Accumulators
PERR
Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Dorel Lucanu , Sebastian Buruiana