{"id":{"repo_id":"cornell","oai_identifier":"oai:ecommons.cornell.edu:1813/114787"},"canonical_url":"https://search.dev.ndltd.org/etd/cornell/oai:ecommons.cornell.edu:1813/114787","repository":{"repo_id":"cornell","name":"Cornell University","base_url":"https://ecommons.cornell.edu/server/oai/request"},"display":{"title":"Lightweight Formal Methods for Correct, Efficient Systems Programming","abstract":"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 lightweight formal methods help us build compilers for fast and reliable computer systems.","abstract_html":"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 lightweight formal methods help us build compilers for fast and reliable computer systems.","abstract_has_math":false,"creators":["VanHattum, Alexa"],"institution":"Cornell University","degree_name":"Ph. D., Computer Science","degree_level":"Doctor of Philosophy","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":["Dell, Nicola","Myers, Andrew"],"year":2023,"date_issued":"2023-08","date_published":"2023-08","updated_at":"2026-07-24T01:49:10Z","subjects":["Compilers","Formal methods","Programming languages"],"languages":["en"],"rights":["Attribution 4.0 International"],"rights_urls":["https://creativecommons.org/licenses/by/4.0/"],"identifier_entries":[{"key":"dc:identifier.doi","label":"DOI","values":["https://doi.org/10.7298/3dd3-da81"],"render_values":[{"text":"https://doi.org/10.7298/3dd3-da81","href":"https://doi.org/10.7298/3dd3-da81","code":true}]},{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["ProQuest Submission ID: 13765","ProQuest Publication ID: 30567888"],"render_values":[{"text":"ProQuest Submission ID: 13765","href":null,"code":true},{"text":"ProQuest Publication ID: 30567888","href":null,"code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/1813/114787","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.committeemember","label":"Committee Member","values":["Dell, Nicola","Myers, Andrew"]},{"key":"dc:creator","label":"Author","values":["VanHattum, Alexa"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2024-04-05T18:48:11Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2024-04-05T18:48:11Z"]},{"key":"dc:date.issued","label":"Date","values":["2023-08"]},{"key":"dc:type","label":"Dc Type","values":["dissertation or thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Doctor of Philosophy"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph. D., Computer Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Cornell University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Compilers","Formal methods","Programming languages"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Attribution 4.0 International"]},{"key":"dc:rights.uri","label":"Rights URI","values":["https://creativecommons.org/licenses/by/4.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.doi","label":"DOI","values":["https://doi.org/10.7298/3dd3-da81"]},{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["ProQuest Submission ID: 13765","ProQuest Publication ID: 30567888"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1813/114787"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["151 pages"]},{"key":"dc:description.abstract","label":"Abstract","values":["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 lightweight formal methods help us build compilers for fast and reliable computer systems."]},{"key":"dc:format.mimetype","label":"Dc Format Mimetype","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Lightweight Formal Methods for Correct, Efficient Systems Programming"]}]}],"canonical_facts":{"dc:contributor.committeemember":["Dell, Nicola","Myers, Andrew"],"dc:creator":["VanHattum, Alexa"],"dc:date.accessioned":["2024-04-05T18:48:11Z"],"dc:date.available":["2024-04-05T18:48:11Z"],"dc:date.issued":["2023-08"],"dc:description":["151 pages"],"dc:description.abstract":["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 lightweight formal methods help us build compilers for fast and reliable computer systems."],"dc:format.mimetype":["application/pdf"],"dc:identifier.doi":["https://doi.org/10.7298/3dd3-da81"],"dc:identifier.other":["ProQuest Submission ID: 13765","ProQuest Publication ID: 30567888"],"dc:identifier.uri":["https://hdl.handle.net/1813/114787"],"dc:language.iso":["en"],"dc:rights":["Attribution 4.0 International"],"dc:rights.uri":["https://creativecommons.org/licenses/by/4.0/"],"dc:subject":["Compilers","Formal methods","Programming languages"],"dc:title":["Lightweight Formal Methods for Correct, Efficient Systems Programming"],"dc:type":["dissertation or thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Doctor of Philosophy"],"thesis:degree_name":["Ph. D., Computer Science"],"thesis:institution_name":["Cornell University"]},"updated_at":"2026-07-24T01:49:10Z"}