arXiv成为独立非营利组织arXiv现已成为独立的非营利组织。论文信息论文《KaniRust的模型检查器》属于计算机科学的软件工程领域编号为arXiv:2607.01504于2026年7月1日提交。作者信息作者包括雷米·德尔马斯Rémi Delmas、扎伊德·哈桑Zyad Hassan、胡沁和平Qinheping Hu等12人。查看方式可查看该论文的PDF版本、HTML实验性版本以及TeX源代码。摘要内容Rust的所有权类型系统可防止安全代码中出现内存错误但某些理想属性仍与编译无关。为此推出了Kani它是用于Rust的开源模型检查器将有界模型检查的应用范围从查找漏洞扩展到为属性提供正确性保证。Kani将Rust的中级中间表示MIR中的证明工具编译到CBMC的位精确验证引擎中无需用户注释即可自动检查一系列全面的安全属性。为将验证从有界扩展到无界Kani提供了一种规范语言。通过对工业级Rust项目的案例研究证明了其可行性发现了六个此前未知的漏洞且在生产环境的持续集成CI中Kani能够大规模运行。评论信息该论文已被第39届IEEE/ACM国际自动化软件工程会议ASE 2026工业展示环节录用主题涉及软件工程 (cs.SE)、计算机科学中的逻辑 (cs.LO)、编程语言 (cs.PL) ACM分类为D.2.4F.3.1 有相应的引用方式。提交历史来自费利佩·R·蒙泰罗于2026年7月1日星期三22:05:33 UTC提交了版本v1文件大小为149 KB。相关工具与资源有文献与引用工具如文献浏览器、关联论文、Litmaps、scite.ai等与本文相关的代码、数据和媒体资源如alphaXiv、代码链接、DagsHub等还有演示相关的如Replicate、Spaces等以及推荐器与搜索工具如影响花链接、CORE推荐器等。arXivLabs介绍arXivLabs是一个框架允许合作者直接在网站上开发和分享新的arXiv功能。与arXivLabs合作的个人和组织需认同并接受开放、社区、卓越和用户数据隐私价值观。若有能为arXiv社区增值的项目想法可了解更多关于arXivLabs的信息。那么Kani在未来的Rust项目验证中还会有怎样的表现和发展呢