Files in this item

FilesDescriptionFormat

application/pdf

application/pdfSEO-THESIS-2015.pdf (239kB)
(no description provided)PDF

Description

Title:Rule-based optimization with K-framework
Author(s):Seo, Seokje
Advisor(s):Padua, David
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:M.S.
Genre:Thesis
Subject(s):Rule-Based
Optimization
K-Framework
pre-compiler
Abstract: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.
Issue Date:2015-10-20
Type:Thesis
URI:http://hdl.handle.net/2142/88962
Rights Information:Copyright 2015 Seokje Seo
Date Available in IDEALS:2016-03-02
Date Deposited:2015-12


This item appears in the following Collection(s)

Item Statistics