Blackbox equivalence checking of program optimizations
Abstract/Contents
- Abstract
- Program equivalence checking is the problem of formally verifying that two programs are equivalent; a key application is verifying the correctness of compiler optimizations. This thesis describes three advances to the state-of-the-art in equivalence checking. The first is a technique called alias relationship mining which helps improve the scalability of equivalence checkers. The second contribution explores the application of equivalence checking to superoptimization, a speculative optimization technique. Lastly, a new technique called semantic program alignment extends the reach of equivalence checking technology to a broader class of problems.
Description
| Type of resource | text |
|---|---|
| Form | electronic resource; remote; computer; online resource |
| Extent | 1 online resource. |
| Place | California |
| Place | [Stanford, California] |
| Publisher | [Stanford University] |
| Copyright date | 2019; ©2019 |
| Publication date | 2019; 2019 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Author | Churchill, Berkeley Roshan |
|---|---|
| Degree supervisor | Aiken, Alexander |
| Thesis advisor | Aiken, Alexander |
| Thesis advisor | Barrett, Clark C |
| Thesis advisor | Mitchell, John C |
| Degree committee member | Barrett, Clark C |
| Degree committee member | Mitchell, John C |
| Associated with | Stanford University, Computer Science Department. |
Subjects
| Genre | Theses |
|---|---|
| Genre | Text |
Bibliographic information
| Statement of responsibility | Berkeley Roshan Churchill. |
|---|---|
| Note | Submitted to the Computer Science Department. |
| Thesis | Thesis Ph.D. Stanford University 2019. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2019 by Berkeley Roshan Churchill
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...