Program (Tuesday 21st July, CAV Slack channel: #workshop-perr)

The workshop will be held online and will start at 6am (Los Angeles), 9am (New York), 2pm (London), 3pm (Paris).

Abstracts

Designing a Self-Certifying Compiler (invited talk):  Compilers are essential to computing but are also amongst the most complex and opaque pieces of software. A compiler gradually lowers a program to executable code while "optimizing" it in various ways. A mistake in any one of these program transformations could produce an executable program that behaves differently from the original. It is very difficult to spot such mistakes through testing. On the other hand, constructing a mathematical proof of the correctness of the compiler code is highly laborious and requires considerable expertise. A "self-certifying" compiler is _designed_ to produce (at compile time) a proof of the correctness of every transformation that it performs on a program. The generated proofs are validated independently and fully automatically. This design dramatically shrinks the trusted code base as only the proof validator must be trusted. As a result, compiler development can proceed (almost) as usual, with the guarantee that any instance of incorrect compilation will be detected by the validator.  I will talk about the theoretical basis for self-certification, our experience with implementing self-certification for LLVM and WebAssembly, and the many intriguing research questions that arise as a result.

Equational Proofs of Optimizations with Interaction Trees:  Proofs are hard to modularize. This talk will describe how the use of equational reasoning, applied to different interpretations of interaction trees, leads to modular proofs about program semantics. Interaction trees take heavy influence from algebraic effects and handlers to obtain modular reasoning principles; are used as a denotational semantic domain for compositionality; and come equipped with combinators supplied with a rich equational theory allowing one to reason up-to weak bisimulation. We present a case study of how using ITrees leads to a crisp separation of concerns and ease of proof-writing in verifying a simple compiler optimization proof.

Relational Test Tables: A Practical Specification Language for Evolution and Security:  A wide range of interesting program properties are relational, i.e., they described a relation between two program runs. Two prominent relational properties are the regression verification (proving conditional program equivalence), and non-interference (proving the absence of information flow). The verification of relational properties is hardly accessible to engineers due to the lack of appropriate specification languages for relational properties. In previous work, we introduced the concept of generalized test tables: a table-based specification language, which allows the tight temporal specification of functional (non-relational) properties for reactive systems. We introduce relational test tables -- an extension of generalized test tables for the specification of relational properties. Relational test tables support specification of k-safety properties (a super set of relational properties) between k>=2 program runs. We show the applicability of relational test tables by specifying and verifying change scenarios and information flow of reactive systems. We provide an implementation of the verification pipeline for programs following the IEC 61131-3 coding standard under http://github.com/VerifAPS/verifaps-lib.

Workshop

PERR is an annual international workshop dedicated to the formal verification of program equivalence and related relational problems. It is the 4th in a series of meetings that bring together researchers from different areas interested in equivalence and related questions. Last year's PERR was held as a satellite workshop of ETAPS. PERR 2020 is affiliated with CAV.

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: denotational semantics, deductive software verification, bounded model checking, specification inference, software evolution and regression testing, etc. The goal of the workshop is to stimulate an exchange of ideas to forge a community working on Program Equivalence and Relational Reasoning (PERR).

The workshop welcomes contributions on the topics mentioned below 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

• 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 online proceedings.

Program Committee

• Vincent Cheval (INRIA Nancy)
• Constantin Enea (Université de Paris)
• Guilhem Jaber (Université de Nantes)
• Nuno Lopes (Microsoft Research Cambridge)
• Andrzej Murawski (University of Oxford)
• Damien Pous (CNRS & ENS Lyon)
• Ofer Strichman (Technion)
• Nikos Tzevelekos (Queen Mary University of London)
• Mattias Ulbrich (KIT)