서브메뉴
검색
Lightweight Formal Methods for Correct, Efficient Systems Programming- [electronic resource]
Lightweight Formal Methods for Correct, Efficient Systems Programming- [electronic resource]
상세정보
- 자료유형
- 학위논문
- Control Number
- 0016933933
- International Standard Book Number
- 9798380317580
- Dewey Decimal Classification Number
- 004
- Main Entry-Personal Name
- VanHattum, Alexa.
- Publication, Distribution, etc. (Imprint
- [S.l.] : Cornell University., 2023
- Publication, Distribution, etc. (Imprint
- Ann Arbor : ProQuest Dissertations & Theses, 2023
- Physical Description
- 1 online resource(152 p.)
- General Note
- Source: Dissertations Abstracts International, Volume: 85-03, Section: B.
- General Note
- Advisor: Sampson, Adrian.
- Dissertation Note
- Thesis (Ph.D.)--Cornell University, 2023.
- Restrictions on Access Note
- This item must not be sold to any third party vendors.
- Summary, Etc.
- 요약Compilers are foundational to everything we ask our computers to do-applications can only be as efficient and reliable as the underlying compiler stack that translates their logic to machine code. But compiler expertise is a finite resource, and engineers may have to choose whether to prioritize adding optimizations for efficiency or validating their existing features for reliability. This dissertation presents three systems that use lightweight, practical formal methods to push past this tension between performance and correctness. The Diospyros compiler combines an efficient term-rewriting strategy, equality saturation, with translation validation to find correct, fast vectorizations for specialized linear algebra tasks on digital signal processors. The Kani verifier for Rust leverages compiler invariants to improve the performance of dynamically dispatched methods in a satisfiability-solver-based model checker for low-level systems code. Finally, the VeriISLE engine uses annotations to automatically verify machine code generation in Cranelift, a popular production compiler infrastructure for WebAssembly where miscompilation bugs can cause serious security vulnerabilities. In sum, these projects point to a future where formal methods help us build compilers for fast and reliable computer systems.
- Subject Added Entry-Topical Term
- Computer science.
- Subject Added Entry-Topical Term
- Computer engineering.
- Index Term-Uncontrolled
- Compilers
- Index Term-Uncontrolled
- Formal methods
- Index Term-Uncontrolled
- Programming languages
- Index Term-Uncontrolled
- Computer systems
- Index Term-Uncontrolled
- Digital signal processors
- Added Entry-Corporate Name
- Cornell University Computer Science
- Host Item Entry
- Dissertations Abstracts International. 85-03B.
- Host Item Entry
- Dissertation Abstract International
- Electronic Location and Access
- 로그인을 한후 보실 수 있는 자료입니다.
- Control Number
- joongbu:639154
MARC
008240219s2023 ulk 00 kor■001000016933933
■00520240214101508
■006m o d
■007cr#unu||||||||
■020 ▼a9798380317580
■035 ▼a(MiAaPQ)AAI30567888
■040 ▼aMiAaPQ▼cMiAaPQ
■0820 ▼a004
■1001 ▼aVanHattum, Alexa.▼0(orcid)0000-0001-6128-8907
■24510▼aLightweight Formal Methods for Correct, Efficient Systems Programming▼h[electronic resource]
■260 ▼a[S.l.]▼bCornell University. ▼c2023
■260 1▼aAnn Arbor▼bProQuest Dissertations & Theses▼c2023
■300 ▼a1 online resource(152 p.)
■500 ▼aSource: Dissertations Abstracts International, Volume: 85-03, Section: B.
■500 ▼aAdvisor: Sampson, Adrian.
■5021 ▼aThesis (Ph.D.)--Cornell University, 2023.
■506 ▼aThis item must not be sold to any third party vendors.
■520 ▼aCompilers are foundational to everything we ask our computers to do-applications can only be as efficient and reliable as the underlying compiler stack that translates their logic to machine code. But compiler expertise is a finite resource, and engineers may have to choose whether to prioritize adding optimizations for efficiency or validating their existing features for reliability. This dissertation presents three systems that use lightweight, practical formal methods to push past this tension between performance and correctness. The Diospyros compiler combines an efficient term-rewriting strategy, equality saturation, with translation validation to find correct, fast vectorizations for specialized linear algebra tasks on digital signal processors. The Kani verifier for Rust leverages compiler invariants to improve the performance of dynamically dispatched methods in a satisfiability-solver-based model checker for low-level systems code. Finally, the VeriISLE engine uses annotations to automatically verify machine code generation in Cranelift, a popular production compiler infrastructure for WebAssembly where miscompilation bugs can cause serious security vulnerabilities. In sum, these projects point to a future where formal methods help us build compilers for fast and reliable computer systems.
■590 ▼aSchool code: 0058.
■650 4▼aComputer science.
■650 4▼aComputer engineering.
■653 ▼aCompilers
■653 ▼aFormal methods
■653 ▼aProgramming languages
■653 ▼aComputer systems
■653 ▼aDigital signal processors
■690 ▼a0984
■690 ▼a0464
■690 ▼a0800
■71020▼aCornell University▼bComputer Science.
■7730 ▼tDissertations Abstracts International▼g85-03B.
■773 ▼tDissertation Abstract International
■790 ▼a0058
■791 ▼aPh.D.
■792 ▼a2023
■793 ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T16933933▼nKERIS▼z이 자료의 원문은 한국교육학술정보원에서 제공합니다.
■980 ▼a202402▼f2024
