Page 325 - 《软件学报》2026年第3期

1288 软件学报 2026 年第 37 卷第 3 期

Int’l Conf. on Agents and Artificial Intelligence. Porto, 2017. 275−286. [doi: 10.5220/0006247302750286]
[30] Wang XZ, Zhang TL, Wang R. Noniterative deep learning: Incorporating restricted Boltzmann machine into multilayer random weight
neural networks. IEEE Trans. on Systems, Man, and Cybernetics: Systems, 2019, 49(7): 1299–1308. [doi: 10.1109/TSMC.2017.2701419]
[31] Mnih V, Kavukcuoglu K, Silver D, Graves A, Antonoglou I, Wierstra D, Riedmiller M. Playing Atari with deep reinforcement learning.
arXiv:1312.5602, 2013.
[32] Zhuang FZ, Luo P, He Q, Shi ZZ. Survey on transfer learning research. Ruan Jian Xue Bao/Journal of Software, 2015, 26(1): 26–39 (in
Chinese with English abstract). http://www.jos.org.cn/1000-9825/4631.htm [doi: 10.13328/j.cnki.jos.004631]
[33] Aravind R, Shah CV. Physics model-based design for predictive maintenance in autonomous vehicles using AI. Int’l Journal of Scientific
Research and Management, 2023, 11(9): 932–946. [doi: 10.18535/ijsrm/v11i09.ec06]
[34] Yokoyama N, Clegg A, Truong J, Undersander E, Yang TY, Arnaud S, Ha S, Batra D, Rai A. ASC: Adaptive skill coordination for
robotic mobile manipulation. IEEE Robotics and Automation Letters, 2024, 9(1): 779–786. [doi: 10.1109/LRA.2023.3336109]
[35] Abbaspour A, Yen KK, Forouzannezhad P, Sargolzaei A. A neural adaptive approach for active fault-tolerant control design in UAV.
IEEE Trans. on Systems, Man, and Cybernetics: Systems, 2020, 50(9): 3401–3411. [doi: 10.1109/TSMC.2018.2850701]
[36] Loveland DW. Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Vol. 6. New York: North-
Holland Publishing Company, 1978.
[37] Clarke EM, Grumberg O, Peled D. Model Checking. Cambridge: MIT Press, 1999.
[38] Clarke EM, Emerson EA, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009,
52(11): 74–84. [doi: 10.1145/1592761.1592781]
[39] Baier C, Katoen JP. Principles of Model Checking. Cambridge: MIT Press, 2008.
[40] Bertot Y, Castéran P. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Berlin:
Springer, 2004. [doi: 10.1007/978-3-662-07964-5]
[41] Paulson LC. Isabelle: The next 700 theorem provers. In: Odifreddi P, ed. Logic and Computer Science. Berlin: Academic Press, 1990.
361–385.
[42] de Moura L, Ullrich S. The Lean 4 theorem prover and programming language. In: Proc. of the 28th Int’l Conf. on Automated Deduction.
Springer, 2021. 625–635. [doi: 10.1007/978-3-030-79876-5_37]
[43] Klein G, Elphinstone KJ, 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 Montana: ACM, 2009. 207–220. [doi: 10.1145/1629575.1629596]
[44] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107–115. [doi: 10.1145/1538788.
1538814]
[45] Wang HM, Yuan Y, Liu ZY, Shen JH, Yin YC, Xiong J, Xie EZ, Shi H, Li Y, Li L, Yin J, Li ZG, Liang XD. DT-solver: Automated
theorem proving with dynamic-tree sampling guided by proof-level value function. In: Proc. of the 61st Annual Meeting of the
Association for Computational Linguistics, Vol. 1 (Long Papers). Toronto: ACL, 2023. 12632–12646. [doi: 10.18653/v1/2023.acl-long.
706]
[46] Liu XP, Liu HZ, Yi XD, Wang J. LLM-enhanced theorem proving with term explanation and tactic parameter repair*. In: Proc. of the
15th Asia-Pacific Symp. on Internetware. Macao: ACM, 2024. 21–30. [doi: 10.1145/3671016.3674823]
[47] Vogel T. mRUBiS: An exemplar for model-based architectural self-healing and self-optimization. In: Proc. of the 13th IEEE/ACM Int’l
Symp. on Software Engineering for Adaptive and Self-managing Systems. Gothenburg: IEEE, 2018. 101–107.
[48] Holzmann GJ. The model checker spin. IEEE Trans. on Software Engineering, 1997, 23(5): 279–295. [doi: 10.1109/32.588521]
[49] Kroening D, Tautschnig M. CBMC-C bounded model checker. 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]
[50] Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S. The NUXMV symbolic model
checker. In: Proc. of the 26th Int’l Conf. on Computer Aided Verification. Vienna, 2014. 334–342. [doi: 10.1007/978-3-319-08867-9_22]
[51] Bradley AR. SAT-based model checking without unrolling. In: Proc. of the 12th Int’l Conf. on Verification, Model Checking, and
Abstract Interpretation. Austin: Springer, 2011. 70–87. [doi: 10.1007/978-3-642-18275-4_7]
[52] Li JW, Zhu SF, Zhang YL, Pu GG, Vardi MY. Safety model checking with complementary approximations. In: Proc. of the 2017
IEEE/ACM Int’l Conf. on Computer-aided Design (ICCAD). Irvine: IEEE, 2017. 95–100. [doi: 10.1109/ICCAD.2017.8203765]
[53] Xia YC, Becchi A, Cimatti A, Griggio A, Li HW, Pu GG. Searching for i-good lemmas to accelerate safety model checking. In: Proc. of
the 35th Int’l Conf. on Computer Aided Verification. Paris: Springer, 2023. 288–308. [doi: 10.1007/978-3-031-37703-7_14]
[54] Su YH, Yang QS, Ci Y. Predicting lemmas in generalization of IC3. In: Proc. of the 61st ACM/IEEE Design Automation Conf. San
Francisco: ACM, 2024. 208. [doi: 10.1145/3649329.3655970]