서브메뉴
검색
Lightweight Formal Methods for Correct, Efficient Systems Programming- [electronic resource]
Lightweight Formal Methods for Correct, Efficient Systems Programming- [electronic resource]
상세정보
- 자료유형
- 학위논문파일 국외
- 최종처리일시
- 20240214101508
- ISBN
- 9798380317580
- DDC
- 004
- 서명/저자
- Lightweight Formal Methods for Correct, Efficient Systems Programming - [electronic resource]
- 발행사항
- [S.l.]: : Cornell University., 2023
- 발행사항
- Ann Arbor : : ProQuest Dissertations & Theses,, 2023
- 형태사항
- 1 online resource(152 p.)
- 주기사항
- Source: Dissertations Abstracts International, Volume: 85-03, Section: B.
- 주기사항
- Advisor: Sampson, Adrian.
- 학위논문주기
- Thesis (Ph.D.)--Cornell University, 2023.
- 사용제한주기
- This item must not be sold to any third party vendors.
- 초록/해제
- 요약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.
- 일반주제명
- Computer science.
- 일반주제명
- Computer engineering.
- 키워드
- Compilers
- 키워드
- Formal methods
- 키워드
- Computer systems
- 기타저자
- Cornell University Computer Science
- 기본자료저록
- Dissertations Abstracts International. 85-03B.
- 기본자료저록
- Dissertation Abstract International
- 전자적 위치 및 접속
- 로그인 후 원문을 볼 수 있습니다.
MARC
008240612s2023 us |||||||||||||||c||eng d■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
