Showing 2025Show all
3 papers · 1 filter
cs.PL2025
A Trace-based Approach for Code Safety Analysis
Hui Xu
Rust is a memory-safe programming language that disallows undefined behavior. Its safety guarantees have been extensively examined by the community through empirical studies, which…
cs.CL2025
KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment
Jiyao Zhang, Chengli Zhong, Hui Xu +2
Modern large language models (LLMs) show promising progress in formalizing informal mathematics into machine-verifiable theorems. However, these methods still face bottlenecks due…
cs.PL2025
Annotating and Auditing the Safety Properties of Unsafe Rust
Zihao Rao, Jiping Zhou, Hongliang Tian +2
In Rust, unsafe code is the sole source of potential undefined behaviors. To avoid misuse, Rust developers should clarify the safety properties for each unsafe API. However, the co…