Péter Bereczky

Machine-checked formal semantics for verifying refactorings!

Peter is an enthusiastic PhD student at Eötvös Loránd University, Budapest. His interests include formal software verification that is why he joined the High-Assurance Refactoring Project, where the goal is to reason about the meaning-preservation of refactorings considering Erlang programs. He is currently working on fomalising Core Erlang and program equivalence in Coq as a stepping stone towards fromalising Erlang.

Program Equivalence in Sequential Core Erlang

AUTHORS: Péter Bereczky and Dániel Horpácsi  

Our research aims to reason about the correctness of scheme-based refactoring transformations of Erlang programs. Recently, we have developed formal semantics for sequential Core Erlang in Coq in order to use it as a stepping stone towards our goal and investigate program transformations in Core Erlang. Refactoring, by definition, means transforming programs to semantically equivalent programs; thus, the correctness of the transformations depends on both the definition of semantics and how we characterize equivalence.  

In this extended abstract, we overview some possible formalisations of expression equivalence for Core Erlang, focusing on different kinds of simple behavioural equivalences which we have already formalised in Coq. We also show some use cases, and outline our short term future plans which include investigating other possible approaches to define program equivalence (for example contextual equivalence, and reasoning about behavioural equivalence using a dedicated logic).

Slides
←Back