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

张卓若 等: 面向 Rust 语言的形式化验证方法研究综述 3633

Programming Languages, 2018, 2(POPL): 66. [doi: 10.1145/3158154]
[14] Bornholt J, Joshi R, Astrauskas V, Cully B, Kragl B, Markle S, Sauri K, Schleit D, Slatton G, Tasiran S, van Geffen J, Warfield A. Using
lightweight formal methods to validate a key-value storage node in Amazon S3. In: Proc. of the 28th ACM SIGOPS Symp. on Operating
Systems Principles. ACM, 2021. 836–850. [doi: 10.1145/3477132.3483540]
[15] Gäher L, Sammler M, Jung R, Krebbers R, Dreyer D. RefinedRust: A type system for high-assurance verification of Rust programs. Proc.
of the ACM on Programming Languages, 2024, 8(PLDI): 192. [doi: 10.1145/3656422]
[16] Ayoun SÉ, Denis X, Maksimović P, Gardner P. A hybrid approach to semi-automated Rust verification. arXiv:2403.15122, 2024.
[17] Polonius. 2019. https://rust-lang.github.io/compiler-team/working-groups/polonius
[18] Huet GP, Kahn G, Paulin-Mohring C. The Coq proof assistant: A tutorial: Version 6.1. 1997. https://inria.hal.science/file/index/docid/
69967/filename/RT-0204.pdf
[19] Matsushita Y, Denis X, Jourdan JH, Dreyer D. RustHornBelt: A semantic foundation for functional verification of Rust programs with
unsafe code. In: Proc. of the 43rd ACM SIGPLAN Int’l Conf. on Programming Language Design and Implementation. San Diego: ACM,
2022. 841–856. [doi: 10.1145/3519939.3523704]
[20] Weiss A, Gierczak O, Patterson D, Ahmed A. Oxide: The essence of Rust. arXiv:1903.00982, 2021.
[21] Lehmann N, Geller AT, Vazou N, Jhala R. Flux: Liquid types for Rust. Proc. of the ACM on Programming Languages, 2023, 7(PLDI):
169. [doi: 10.1145/3591283]
[22] Payet É, Pearce DJ, Spoto F. On the termination of borrow checking in featherweight Rust. In: Proc. of the 14th Int’l Symp. on NASA
Formal Methods. Pasadena: Springer, 2022. 411–430. [doi: 10.1007/978-3-031-06773-0_22]
[23] Reed E. Patina: A formalization of the Rust programming language. Technical Report, UW-CSE-15-03-02, Washington: University of
Washington, 2015.
[24] Jung R, Dang HH, Kang J, Dreyer D. Stacked borrows: An aliasing model for Rust. Proc. of the ACM on Programming Languages, 2020,
4(POPL): 41. [doi: 10.1145/3371109]
[25] Wang F, Song F, Zhang M, Zhu XR, Zhang J. KRust: A formal executable semantics of Rust. In: Proc. of the 2018 Int’l Symp. on
Theoretical Aspects of Software Engineering. Guangzhou: IEEE, 2018. 44–51. [doi: 10.1109/TASE.2018.00014]
[26] Kan SL, Chen Z, Sanan D, Lin SW, Liu Y. An executable operational semantics for Rust with the formalization of ownership and
borrowing. arXiv:1804.07608, 2020.
[27] Cardelli L. Type systems. ACM Computing Surveys (CSUR), 1996, 28(1): 263–264. [doi: 10.1145/234313.234418]
[28] Igarashi A, Pierce BC, Wadler P. Featherweight Java: A minimal core calculus for Java and GJ. ACM Trans. on Programming Languages
and Systems (TOPLAS), 2001, 23(3): 396–450. [doi: 10.1145/503502.503505]
[29] Jung R, Swasey D, Sieczkowski F, Svendsen K, Turon A, Birkedal L, Dreyer D. Iris: Monoids and invariants as an orthogonal basis for
concurrent reasoning. In: Proc. of the 42nd Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Mumbai:
ACM, 2015. 637–650. [doi: 10.1145/2676726.2676980]
[30] Jung R, Krebbers R, Jourdan JH, Bizjak A, Birkedal L, Dreyer D. Iris from the ground up: A modular foundation for higher-order
concurrent separation logic. Journal of Functional Programming, 2018, 28: e20. [doi: 10.1017/S0956796818000151]
[31] Dang HH, Jourdan JH, Kaiser JO, Dreyer D. RustBelt meets relaxed memory. Proc. of the ACM on Programming Languages, 2020,
4(POPL): 34. [doi: 10.1145/3371102]
[32] Sammler M, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. RefinedC: Automating the foundational verification of C code with
refined ownership types. In: Proc. of the 42nd ACM SIGPLAN Int’l Conf. on Programming Language Design and Implementation.
Virtual: ACM, 2021. 158–174. [doi: 10.1145/3453483.3454036]
[33] Astrauskas V, Müller P, Poli F, Summers AJ. Leveraging Rust types for modular specification and verification. Proc. of the ACM on
Programming Languages, 2019, 3(OOPSLA): 147. [doi: 10.1145/3360573]
[34] Lattuada A, Hance T, Cho C, Brun M, Subasinghe I, Zhou Y, Howell J, Parno B, Hawblitzel C. Verus: Verifying Rust programs using
linear ghost types. Proc. of the ACM on Programming Languages, 2023, 7(OOPSLA1): 85. [doi: 10.1145/3586037]
[35] Denis X, Jourdan JH, Marché C. CREUSOT: A foundry for the deductive verification of Rust programs. In: Proc. of the 23rd Int’l Conf.
on Formal Methods and Software Engineering: Int’l Conf. on Formal Engineering Methods. Madrid: Springer, 2022. 90–105. [doi: 10.
1007/978-3-031-17244-1_6]
[36] Matsushita Y, Tsukada T, Kobayashi N. RustHorn: CHC-based verification for Rust programs. ACM Trans. on Programming Languages
and Systems (TOPLAS), 2021, 43(4): 15. [doi: 10.1145/3462205]
[37] Jacobs B, Smans J, Philippaerts P, Vogels F, Penninckx W, Piessens F. VeriFast: A powerful, sound, predictable, fast verifier for C and
Java. In: Proc. of the 3rd Int’l Conf. on NASA Formal Methods. Pasadena: Springer, 2011. 41–55. [doi: 10.1007/978-3-642-20398-5_4]