Files in this item

FilesDescriptionFormat

application/pdf

application/pdfMIRANTI-THESIS-2020.pdf (259kB)
(no description provided)PDF

Description

Title:Semantics of low-level languages
Author(s):Miranti, Andrew
Advisor(s):Rosu, Grigore
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:M.S.
Genre:Thesis
Subject(s):Semantics
K Framework
x86
Tezos
Michelson
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.
Issue Date:2020-05-12
Type:Thesis
URI:http://hdl.handle.net/2142/108037
Rights Information:Copyright 2020 Andrew Miranti
Date Available in IDEALS:2020-08-26
Date Deposited:2020-05


This item appears in the following Collection(s)

Item Statistics