Rust is a relatively new programming language with a unique memory model designed to provide the ease of use of a high-level language as well as the power and control of a low-level language while preserving memory safety. In order to prove the safety and correctness of Rust and to provide analysis tools for its use cases, it is necessary to construct a formal semantics of the language. Existing efforts to construct such a semantic model are limited in their scope and none to date have successfully captured the complete functionality of the language. This thesis focuses on the K-Rust implementation, which is implemented in a rewrite-based semantic framework called K, and expands it to include a larger subset of the Rust language. The K framework allows Rust programs to be executed by the defined semantic model, and the implementation is tested with several Rust programs by comparing the results of execution to the Rust compiler itself.
| Identifer | oai:union.ndltd.org:CALPOLY/oai:digitalcommons.calpoly.edu:theses-3804 |
| Date | 01 March 2021 |
| Creators | White, Alexa |
| Publisher | DigitalCommons@CalPoly |
| Source Sets | California Polytechnic State University |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | Master's Theses |
Page generated in 0.0023 seconds