While the Rust language provides memory safety by default, functional correctness and safety of programs using unsafe code remain unchecked. This thesis aims to improve the quality of Rust code and assist adoption of Rust by developing automatic testing and verification techniques for analyzing properties unchecked by the language. For testing unsafe library APIs, we develop Rust semantic-aware synthesizers that generate well-typed Rust API calls to efficiently search through the state space guided by types. We develop SyRust (PLDI’21), a synthesizer equipped with awareness of the Rust type semantics. Semantic awareness allows SyRust to generate well-typed API tests for polymorphic Rust library APIs and find memory safety bugs in them. To overcome the scalability limitations of SyRust on large API sets found in popular libraries, we develop Crabtree (OOPSLA’24), a heuristic-guided API test synthesis algorithm that leverages code coverage and coverage over Rust types to guide the synthesis of tests. Results indicate Crabtree yields higher and quicker code coverage over SyRust. We also develop automatic tools for lightweight Rust verification and testing of less explored properties such as developer-annotated assertions, trait invariants, and translation equivalence.

Yoshiki Takashima is a postdoc at Yale Law School applying formal and automated reasoning to law. He received his Ph.D. from CMU in 2024 with a dissertation focusing on testing and verification tools that leverage properties of the Rust programming language.