자료유형  

 학위논문

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