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

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

本文提出的方法在实际验证中体现出的优势包括: (1) 验证模块化更明显; (2) 验证代码的可拓展性更强. 但本
文的验证有一定的局限性, 包括代码的精化关系未进行正式形式化验证; 接口本身的可靠性未正式验证. 这些局限
性也是后续工作的一部分.

References:
[1] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1): 33–61 (in
Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm [doi: 10.13328/j.cnki.jos.005652]
[2] Liang HJ, Feng XY, Fu M. Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM
Trans. on Programming Languages and Systems (TOPLAS), 2014, 36(1): 3. [doi: 10.1145/2576235]
[3] Xu FW, Fu M, Feng XY, Zhang XR, Zhang H, Li ZH. A practical verification framework for preemptive OS kernels. In: Proc. of the 28th
Int’l Conf. on Computer Aided Verification. Toronto: Springer, 2016. 59–79. [doi: 10.1007/978-3-319-41540-6_4]
[4] Qiao L, Yang MF, Tan YL, Pu GG, Yang H. Formal verification of memory management system in spacecraft using Event-B. Ruan Jian
Xue Bao/Journal of Software, 2017, 28(5): 1204–1220 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5218.htm
[doi: 10.13328/j.cnki.jos.005218]
[5] Ghosh D, Tomazeli L, Jin F, Maheswaran M. SpaceOS: Operating system services for smart computing environments. In: Proc. of the
2014 IEEE Int’l Symp. on a World of Wireless, Mobile and Multimedia Networks. Sydney: IEEE, 2014. 1–6. [doi: 10.1109/WoWMoM.
2014.6918932]
[6] Klein G, Huuck R, Schlich B. Operating system verification. Journal of Automated Reasoning, 2009, 42(1): 123–124. [doi: 10.1007/
s10817-009-9126-9]
[7] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H,
Winwood S. seL4: Formal verification of an OS kernel. In: Proc. of the 22nd ACM SIGOPS Symp. on Operating Systems Principles. Big
Sky: ACM, 2009. 207–220. [doi: 10.1145/1629575.1629596]
[8] Andronick J, Lewis C, Morgan C. Controlled owicki-gries concurrency: Reasoning about the preemptible eChronos embedded operating
system. In: Electronic Proc. in Theoretical Computer Science. Open Publishing Association, 2015. 10–24. [doi: 10.4204/EPTCS.196.2]
[9] Hunt GC, Larus JR. Singularity: Rethinking the software stack. ACM SIGOPS Operating Systems Review, 2007, 41(2): 37–49. [doi: 10.
1145/1243418.1243424]
[10] Cui MH, Chen CJ, Xu H, Zhou YF. SafeDrop: Detecting memory deallocation bugs of Rust programs via static data-flow analysis. ACM
Trans. on Software Engineering and Methodology, 2023, 32(4): 82. [doi: 10.1145/3542948]
[11] Dai ZY, Liu S, Sjoberg V, Li XP, Chen Y, Wang WH, Jia YK, Anderson SN, Elbeheiry L, Sondhi S, Zhang Y, Ni ZZ, Yan SM, Gu RH,
He ZY. Verifying Rust implementation of page tables in a software enclave hypervisor. In: Proc. of the 29th ACM Int’l Conf. on
Architectural Support for Programming Languages and Operating Systems. La Jolla: ACM, 2024. 1218–1232. [doi: 10.1145/3620665.
3640398]
[12] 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 (ASE). Lincoln: IEEE, 2015. 75–80. [doi: 10.1109/ASE.2015.77]
[13] Kroening D, Tautschnig M. CBMC-C bounded model checker (competition contribution). In: Proc. of the 20th Int’l Conf. on Tools and
Algorithms for the Construction and Analysis of Systems. Grenoble: Springer, 2014. 389–391. [doi: 10.1007/978-3-642-54862-8_26]
[14] Vytautas A, 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]
[15] Schilling J. Specifying and verifying sequences and array algorithms in a Rust verifier [MS. Thesis]. Zürich: Eidgenössische Technische
Hochschule Zürich, 2021.
[16] Jung R, Jourdan JH, Krebbers R, Dreyer D. RustBelt: Securing the foundations of the Rust programming language. Proc. of the ACM on
Programming Languages, 2018, 2(POPL): 66. [doi: 10.1145/3158154]
[17] Yanovski J, Dang HH, Jung R, Dreyer D. GhostCell: Separating permissions from data in Rust. Proc. of the ACM on Programming
Languages, 2021, 5(ICFP): 92. [doi: 10.1145/3473597]
[18] 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 (PLDI 2022). San
Diego: ACM, 2022. 841–856. [doi: 10.1145/3519939.3523704]
[19] Paulin-Mohring C. Introduction to the Coq proof-assistant for practical software verification. In: Meyer B, Nordio M, eds. Tools for
Practical Software Verification. Berlin: Springer, 2012. 45–95. [doi: 10.1007/978-3-642-35746-6_3]