Péter Bereczky

Student, student lecturer, interested in formal verification

Peter is an enthusiastic MSc student and a student lecturer at Eötvös Loránd University, Budapest. He has a BSc in Computer Science from the same university. His interests include formal software verification that is why he joined a software technology lab, where the goal is to reason about the meaning-preservation of refactoring tools.

A Proof Assistant Based Formalisation of Core Erlang

How can we reason about the correctness of source code transformations, refactorings on a programming language? First, a mathematically rigoruos description of that language is needed. In this talk we present such a formal definition of sequential Core Erlang which is also formalised in Coq. In addition we also show how to build and use this definition to prove the meaning-preservation of refactorings.

Slides
Video ←Back