{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/108037"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/108037","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Miranti, Andrew"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Rosu, Grigore"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2020,"date_issued":"2020-08-26T21:58:03Z","date_published":"2020-08-26T21:58:03Z","updated_at":"2026-07-22T22:24:47Z","subjects":["Semantics","K Framework","x86","Tezos","Michelson"],"languages":["en"],"rights":["Copyright 2020 Andrew Miranti"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/108037","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Rosu, Grigore"]},{"key":"dc:creator","label":"Author","values":["Miranti, Andrew"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2020-08-26T21:58:03Z","2020-05-12","2020-05"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Semantics","K Framework","x86","Tezos","Michelson"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2020 Andrew Miranti"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/108037"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Semantics of low-level languages"]}]}],"canonical_facts":{"dc:contributor":["Rosu, Grigore"],"dc:creator":["Miranti, Andrew"],"dc:date":["2020-08-26T21:58:03Z","2020-05-12","2020-05"],"dc:description":["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"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/108037"],"dc:language":["en"],"dc:rights":["Copyright 2020 Andrew Miranti"],"dc:subject":["Semantics","K Framework","x86","Tezos","Michelson"],"dc:title":["Semantics of low-level languages"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:47Z"}