A Formal Semantics of BEAM Bytecode

Erlang is a high-level functional programming language. Its run-time system is designed for distributed, fault-tolerant and highly available systems. Originally developed for telephony switches by Ericsson, the language is now in use in a wide range of industries - for instance, WhatsApp is written in Erlang.

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.

Work environment:
Isabelle (Windows/macOS/Linux)
Useful knowledge/skills:
Functional programming, first-order logic, programming language semantics
Tjark Weber

Last modified: 2023-11-05