2026-09-19T09:01:23Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/88962 2023-07-11 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Padua, David Seo, Seokje 2016-03-02T19:33:21Z 2016-03-02T19:33:21Z 2015-10-20 2015-12 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. Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2016-03-02 without embargo terms The student, Seokje Seo, accepted the attached license on 2015-10-17 at 02:41. The student, Seokje Seo, submitted this Thesis for approval on 2015-10-19 at 13:16. This Thesis was approved for publication on 2015-10-20 at 14:34. DSpace SAF Submission Ingestion Package generated from Vireo submission #8726 on 2016-03-02 at 12:49:33 Made available in DSpace on 2016-03-02T19:33:21Z (GMT). No. of bitstreams: 2 SEO-THESIS-2015.pdf: 238922 bytes, checksum: 454dedb65b9e2cf1b927324a59a722cc (MD5) LICENSE.txt: 4207 bytes, checksum: c3f2be2e52a12ea388cd52e608ad17be (MD5) Previous issue date: 2015-10-20 application/pdf http://hdl.handle.net/2142/88962 en Copyright 2015 Seokje Seo Rule-Based Optimization K-Framework pre-compiler Rule-based optimization with K-framework text text Computer Science Computer Science University of Illinois at Urbana-Champaign Thesis M.S.