2 papers
cs.SE2026
HarnessLLM: Rust Verification Harness Generation with Large Language Models
Minghua Wang, Yuwei Liu, Lin Huang
Rust's ownership model and type system offer strong memory safety guarantees, but unsafe code and runtime panics still present significant risks. Formal verification is essential t…
cs.SE2026
KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
Minghua Wang, Yuxi Ling, Mingzhi Gao +2
Rust's ownership and type system provide strong memory safety guarantees, but unsafe code still presents memory safety risks. Formal verification is crucial for ensuring memory saf…