Semantics of low-level languages

Abstract

In this paper we address the motivations, problems and challenges involved in formally specifying low level programming languages. We utilize the K programming language specification framework to build executable models of the languages discussed: x86 and Tezos Michelson. We extend an existing formalization of x86 to include its most common format - executable binaries by implementing an instruction decoder. We start completely from scratch with another: Tezos’ Michelson. We produce executable models capable of running programs in each language, with natural extensions towards formal verification tools possible through the K Framework. Finally, we discuss the differences between the two languages which make formalizing the former daunting, and the latter relatively straightforward.