Erlang source code is compiled into bytecode by the Erlang compiler. This bytecode is then executed by the BEAM virtual machine that is an integral part of the Erlang run-time system.
The goal of this project is to formally define the semantics of (a subset of) BEAM bytecode in the interactive proof assistant Isabelle. Isabelle is a software tool that allows pogramming languages and their semantics to be defined in a formal logic. This logic offers both concepts from programming (e.g., datatypes, recursive functions) and mathematical concepts (e.g., quantifiers).
This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.