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.
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.
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.
Sat 6 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:30
|Invited talk by Margus Veanes|
Margus Veanes Microsoft Research
|Local Reasoning for Robust Observational Equivalence|
Dan Ghica University of Birmingham, Koko Muroya RIMS, Kyoto University, JP & University of Birmingham, UK, Todd Waugh Ambridge University of Birmingham
11:00 - 12:30
|Understanding Counterexamples for Relational Properties with DIbugger|
Mihai Herda , Michael Kirsten Karlsruhe Institute of Technology (KIT), Etienne Brunner , Joana Plewnia , Ulla Scheler , Chiara Staudenmaier , Benedikt Wagner , Pascal Zwick , Bernhard Beckert Karlsruhe Institute of Technology
|Analysis of program differences with numerical abstract interpretation|
David Delmas Airbus & Sorbonne Université, Antoine Miné UPMC, FranceLink to publication Pre-print File Attached
|On Quantitative Comparison of Chemical Reaction Network Models|
14:00 - 15:30
|Invited talk by Marco Eilers|
Marco Eilers ETH Zurich
|Relational Verification via Invariant-Guided Synchronization|
16:00 - 18:00
|Automatic Equivalence Proofs for Programs with Algebraic Data Types|
Moritz Kiefer , Mattias Ulbrich Karlsruhe Institute of Technology
|Proving Program Equivalence with Constrained Rewriting Induction and Ctrl|
Carsten Fuhs Birkbeck, University of London, Cynthia Kop Radboud University Nijmegen, Naoki Nishida Nagoya University
|Semantics-Based Proofs of Equivalence for Functions with Accumulators|
Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Dorel Lucanu , Sebastian Buruiana