Files in this item
Files | Description | Format |
---|---|---|
application/pdf ![]() | (no description provided) |
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)
-
Dissertations and Theses - Computer Science
Dissertations and Theses from the Dept. of Computer Science -
Graduate Dissertations and Theses at Illinois
Graduate Theses and Dissertations at Illinois