Semantics of low-level languages

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.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2020

Author dc:creator

• Miranti, Andrew

Contributors dc:contributor

• Rosu, Grigore

• Semantics
• K Framework
• x86
• Tezos
• Michelson

Statement dc:rights

• Copyright 2020 Andrew Miranti

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/108037

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/108037