2026-09-19T16:09:51Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/108037 2023-07-11 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Rosu, Grigore Miranti, Andrew 2020-08-26T21:58:03Z 2020-08-26T21:58:03Z 2020-05-12 2020-05 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. Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2020-08-25 without embargo terms The student, Andrew Miranti, accepted the attached license on 2020-05-11 at 15:51. The student, Andrew Miranti, submitted this Thesis for approval on 2020-05-11 at 15:56. This Thesis was approved for publication on 2020-05-12 at 10:06. DSpace SAF Submission Ingestion Package generated from Vireo submission #15332 on 2020-08-25 at 17:13:58 Made available in DSpace on 2020-08-26T21:58:03Z (GMT). No. of bitstreams: 3 MIRANTI-THESIS-2020.pdf: 258685 bytes, checksum: 1e494df33d527ed91e94c7dc072de5c8 (MD5) MirantiThesisSource.zip: 80234 bytes, checksum: 2a3ba4539bde3b3f977712f4f678e893 (MD5) LICENSE.txt: 4211 bytes, checksum: 52b8f7b4ddc8e8fb0cd6891fa90a80e4 (MD5) Previous issue date: 2020-05-12 application/pdf http://hdl.handle.net/2142/108037 en Copyright 2020 Andrew Miranti Semantics K Framework x86 Tezos Michelson Semantics of low-level languages text Thesis Computer Science Computer Science University of Illinois at Urbana-Champaign Thesis M.S.