Director of Research (if dissertation) or Advisor (if thesis)
Padua, David
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
M.S.
Degree Level
Thesis
Keyword(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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
