Rule-based optimization with K-framework

The thesis discusses pre-compiler optimization using rule-based rewriting. Our goal is to facilitate the proof of correctness of the process of program optimization. A source-to-source optimizer based on the proposed strategy can be a preprocessor to a certified compiler such as CompCert and this way it will facilitate the process of certification of a sophisticated compiler. In fact, CompCert is highly assured but it trades off the assurance with efficiency. Unlike other compilers like Intel C compiler or GNU C compiler, CompCert does not optimize aggressively. The paper will discuss optimization rules implemented using the K-framework and how much efficiency improvement achieved by use of our optimization rules.

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

2016

Author dc:creator

• Seo, Seokje

Contributors dc:contributor

• Padua, David

• Rule-Based
• Optimization
• K-Framework
• pre-compiler

Statement dc:rights

• Copyright 2015 Seokje Seo

Language dc:language

en

Handle dc:identifier

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

OAI identifier oai:identifier

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