1 option
Modular Semantics and Metatheory for LLVM IR / Euisun Yoon.
- Format:
- Book
- Thesis/Dissertation
- Author/Creator:
- Yoon, Euisun, author.
- Language:
- English
- Subjects (All):
- Computer science.
- Computer engineering.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Local Subjects:
- Computer science.
- Computer engineering.
- Computer and Information Science--Penn dissertations.
- Penn dissertations--Computer and Information Science.
- Physical Description:
- 1 online resource (169 pages)
- Distribution:
- Ann Arbor : ProQuest Dissertations & Theses, 2023
- Contained In:
- Dissertations Abstracts International 85-08B.
- Place of Publication:
- [Philadelphia, Pennsylvania] : University of Pennsylvania, 2022.
- Language Note:
- English
- Summary:
- The appealing guarantees of formally verified software comes in tandem with the high cost of verification. To reduce the cost of formal verification, modularity is crucial because it eases both the elaboration and reuse of proofs. This thesis focuses on developing a modular semantics and metatheory for realistic low-level languages, with a focus on LLVM IR. First, we define VIR, a modular and executable semantics for a large sequential subset of LLVM IR, which is based on layered, monadic interpreters. Unlike a traditional small-step semantics, VIR has an executable semantics which can be extracted into an executable definitional interpreter. Second, we develop a formal metatheory for reasoning about layered interpreters, giving an extensible theory for lifting interpreters and structural rules, characterizing interpretable monads and a relational reasoning framework for reasoning about equivalences across interpretation. Finally, we develop a relational separation logic framework for verifying program transformations on VIR, with a fresh perspective on verifying transformations with external calls.
- Notes:
- Source: Dissertations Abstracts International, Volume: 85-08, Section: B.
- Advisors: Zdancewic, Stephan A.; Committee members: Pierce, Benjamin C.; Weirich, Stephanie; Tannen, Val B.; Dreyer, Derek.
- Department: Computer and Information Science.
- Ph.D. University of Pennsylvania 2023.
- Local Notes:
- School code: 0175
- ISBN:
- 9798381472042
- Access Restriction:
- Restricted for use by site license.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.