Page 211 - 《软件学报》2025年第8期

3634 软件学报 2025 年第 36 卷第 8 期

[38] Toman J, Pernsteiner S, Torlak E. Crust: A bounded verifier for Rust (N). In: Proc. of the 30th IEEE/ACM Int’l Conf. on Automated
Software Engineering. Lincoln: IEEE, 2015. 75–80. [doi: 10.1109/ASE.2015.77]
[39] Baranowski M, He SB, Rakamarić Z. Verifying Rust programs with SMACK. In: Proc. of the 16th Int’l Symp. on Automated Technology
for Verification and Analysis. Los Angeles: Springer, 2018. 528–535. [doi: 10.1007/978-3-030-01090-4_32]
[40] Kani Rust verifier. 2022. https://github.com/model-checking/kani
[41] Loom. 2021. https://github.com/tokio-rs/loom?tab=readme-ov-file
[42] Zhang KW, Liu GJ. Automatically transform Rust source to Petri nets for checking deadlocks. arXiv:2212.02754, 2022.
[43] Ullrich S. Simple verification of Rust programs via functional purification [MS. Thesis]. Karlsruhe: Karlsruhe Institute of Technology,
2016.
[44] Ho S, Protzenko J. Aeneas: Rust verification by functional translation. Proc. of the ACM on Programming Languages, 2022, 6(ICFP):
116. [doi: 10.1145/3547647]
[45] Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symp. on Logic in
Computer Science. Copenhagen: IEEE, 2002. 55–74. [doi: 10.1109/LICS.2002.1029817]
[46] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576–580. [doi: 10.1145/363235.
363259]
[47] de Moura L, Bjørner N. Z3: An efficient SMT solver. In: Proc. of the 14th Int’l Conf. on Tools and Algorithms for the Construction and
Analysis of Systems. Budapest: Springer, 2008. 337–340. [doi: 10.1007/978-3-540-78800-3_24]
[48] Müller P, Schwerhoff M, Summers AJ. Viper: A verification infrastructure for permission-based reasoning. In: Proc. of the 17th Int’l
Conf. on Verification, Model Checking, and Abstract Interpretation. Petersburg: Springer, 2016. 41–62. [doi: 10.1007/978-3-662-49122-
5_2]
[49] Foroushaani NR, Jacobs B. Modular formal verification of Rust programs with unsafe blocks. arXiv:2212.12976, 2022.
[50] Fragoso Santos J, Maksimović P, Ayoun SÉ, Gardner P. Gillian, part I: A multi-language platform for symbolic execution. In: Proc. of
the 41st ACM SIGPLAN Conf. on Programming Language Design and Implementation. London: ACM, 2020. 927–942. [doi: 10.1145/
3385412.3386014]
[51] Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Berlin: Springer, 2002.
[52] Avigad J, De Moura L, Kong S. Theorem proving in Lean. 2024. https://leanprover.github.io/theorem_proving_in_lean/theorem_
proving_in_lean.pdf
[53] Clarke E, Kroening D, Lerda F. A tool for checking ANSI-C programs. In: Proc. of the 10th Int’l Conf. on Tools and Algorithms for the
Construction and Analysis of Systems. Barcelona: Springer, 2004. 168–176. [doi: 10.1007/978-3-540-24730-2_15]
[54] Byrnes T, Takashima Y, Jia LM. Automatically enforcing Rust trait properties. In: Proc. of the 25th Int’l Conf. on Verification, Model
Checking, and Abstract Interpretation. London: Springer, 2024. 210–223. [doi: 10.1007/978-3-031-50521-8_10]
[55] Thurrott P. Microsoft is rewriting parts of the windows kernel in Rust. 2023. https://www.thurrott.com/windows/282471/microsoft-is-
rewriting-parts-of-the-windows-kernel-in-rust
[56] Rust for Linux. 2024. https://github.com/Rust-for-Linux
[57] Jansens D. Supporting the use of Rust in the Chromium project. 2023. https://security.googleblog.com/2023/01/supporting-use-of-rust-in-
chromium.html
[58] Stoep JV, Chrome Security Team. Memory safe languages in Android 13. 2022. https://security.googleblog.com/2022/12/memory-safe-
languages-in-android-13.html
[59] Narayanan V, Baranowski MS, Ryzhyk L, Rakamarić Z, Burtsev A. RedLeaf: Towards an operating system for safe and verified
firmware. In: Proc. of the 2019 Workshop on Hot Topics in Operating Systems. Bertinoro: ACM, 2019. 37–44. [doi: 10.1145/3317550.
3321449]
[60] Brun M, Achermann R, Chajed T, Howell J, Zellweger G, Lattuada A. Beyond isolation: OS verification as a foundation for correct
applications. In: Proc. of the 19th Workshop on Hot Topics in Operating Systems. Providence: ACM, 2023. 158–165. [doi: 10.1145/
3593856.3595899]
[61] Bhardwaj A, Kulkarni C, Achermann R, Calciu I, Kashyap S, Stutsman R, Tai A, Zellweger G. NrOS: Effective replication and sharing in
an operating system. In: Proc. of the 15th USENIX Symp. on Operating Systems Design and Implementation. USENIX Association,
2021. 295–312.
[62] Chen XD, Li ZF, Mesicek L, Narayanan V, Burtsev A. Atmosphere: Towards practical verified kernels in Rust. In: Proc. of the 1st
Workshop on Kernel Isolation, Safety and Verification. Koblenz: ACM, 2023. 9–17. [doi: 10.1145/3625275.3625401]
[63] Ijaz R, Boos K, Zhong L. Leveraging Rust for lightweight OS correctness. In: Proc. of the 1st Workshop on Kernel Isolation, Safety and