Closing the gap in the LLVM backend of K

In this thesis, we further develop part of the K framework, a framework for specifying and executing the formal semantics of languages. We dive into the LLVM backend, one of the engines for concrete execution, and implement key functionality that is present in the other concrete execution engine. We then add a new interface that is unique to the LLVM backend, making this backend diverge from the other backend. Finally, with the backend caught up and divergent, we implement and evaluate pattern matching optimization strategies.

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

• Abir, Michael

Contributors dc:contributor

• Rosu, Grigore

• programming languages, rewriting-based execution, optimization

Statement dc:rights

• Copyright 2020 Michael Abir

Language dc:language

en

Handle dc:identifier

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

OAI identifier oai:identifier

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