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

徐雄 等: 嵌入式软件 IP 通用模型 1263

[94] Xu FF, Vasilescu B, Neubig G. In-IDE code generation from natural language: Promise and challenges. ACM Trans. on Software
Engineering and Methodology (TOSEM), 2022, 31(2): 29. [doi: 10.1145/3487569]
[95] Yan GG, Jiao L, Wang SL, Wang LT, Zhan NJ. Automatically generating systemc code from HCSP formal models. ACM Trans. on
Software Engineering and Methodology (TOSEM), 2020, 29(1): 4. [doi: 10.1145/3360002]
[96] Wang SL, Ji ZK, Xu X, Zhan BH, Gao Q, Zhan NJ. Formally verified C code generation from hybrid communicating sequential
processes. In: Proc. of the 15th ACM/IEEE Int’l Conf. on Cyber-physical Systems. Hong Kong: IEEE, 2024. 123–134. [doi: 10.1109/
ICCPS61052.2024.00018]
[97] Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C. The Daikon system for dynamic detection of likely
invariants. Science of Computer Programming, 2007, 69(1–3): 35–45. [doi: 10.1016/j.scico.2007.01.015]
[98] Molina F, Ponzio P, Aguirre N, Frias M. EvoSpex: An evolutionary algorithm for learning postconditions. In: Proc. of the 43rd
IEEE/ACM Int’l Conf. on Software Engineering. Madrid: IEEE, 2021. 1223–1235. [doi: 10.1109/ICSE43902.2021.00112]
[99] Pei KX, Bieber D, Shi KS, Sutton C, Yin PC. Can large language models reason about program invariants? In: Proc. of the 40th Int’l
Conf. on Machine Learning. Honolulu: PMLR, 2023. 27496–27520.
[100] Alpuente M, Pardo D, Villanueva A. Abstract contract synthesis and verification in the symbolic K framework. Fundamenta
Informaticae, 2020, 177(3–4): 235–273. [doi: 10.3233/FI-2020-1989]
[101] Blasi A, Goffi A, Kuznetsov K, Gorla A, Ernst MD, Pezzè M, Castellanos SD. Translating code comments to procedure specifications.
In: Proc. of the 27th ACM SIGSOFT Int’l Symp. on Software Testing and Analysis. Amsterdam: ACM, 2018. 242–253. [doi: 10.1145/
3213846.3213872]
[102] Jackson D. The Essence of Software: Why Concepts Matter for Great Design. Princeton: Princeton University Press, 2021.
[103] Alpuente M, Feliú MA, Villanueva A. Automatic inference of specifications using matching logic. In: Proc. of the 2013 ACM
SIGPLAN Workshop on Partial Evaluation and Program Manipulation. Rome: ACM, 2013. 127–136. [doi: 10.1145/2426890.2426914]
[104] Wen C, Cao JL, Su J, Xu ZW, Qin SC, He MD, Li HK, Cheung SC, Tian C. Enchanting program specification synthesis by large
language models using static analysis and program verification. In: Proc. of the 36th Int’l Conf. on Computer Aided Verification.
Montreal: Springer, 2024. 302–328. [doi: 10.1007/978-3-031-65630-9_16]
[105] Baudin P, Filliâtre JC, Marché C, Monate B, Moy Y, Prevosto V. ACSL: ANSI C specification language. Technical Report, v1.2, CEA-
list, 2008.
[106] Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B. Frama-C: A software analysis perspective. Formal Aspects of
Computing, 2015, 27(3): 573–609. [doi: 10.1007/s00165-014-0326-7]

附中文参考文献
[14] 杨孟飞, 顾斌, 段振华, 金芝, 詹乃军, 董云卫, 田聪, 李戈, 董晓刚, 李晓锋. 嵌入式软件智能合成框架及关键科学问题. 中国空间科
学技术, 2022, 42(4): 1–7. [doi: 10.16708/j.cnki.1000-758X.2022.0046]
[81] 陆汝钤, 金芝. 从基于知识的软件工程到基于知件的软件工程. 中国科学 E 辑: 信息科学, 2008, 38(6): 843–863. [doi: 10.1360/zf2008-
38-6-843]
[83] 国家市场监督管理总局, 国家标准化管理委员会. GB/T 36455-2018 软件构件模型. 北京: 中国标准出版社, 2018.

作者简介
徐雄, 博士, 助理研究员, 主要研究领域为信息物理融合系统设计, 模型驱动开发, 形式化方法.
马旭, 硕士生, 主要研究领域为软件工程, 形式化方法.
高强, 硕士, 主要研究领域为形式化方法.
计泽坤, 硕士, 主要研究领域为形式化方法.
王淑灵, 博士, 副研究员, CCF 专业会员, 主要研究领域为信息物理融合系统形式验证.
詹博华, 博士, CCF 专业会员, 主要研究领域为形式化方法, 定理证明, 程序验证.
詹乃军, 博士, 教授, 博士生导师, CCF 杰出会员, 主要研究领域为信息物理融合系统设计, 程序验证, 模态和时序逻辑.
李晓锋, 研究员, CCF 专业会员, 主要研究领域为嵌入式高可信软件开发, 软件缺陷检测, 软件智能开发.
顾斌, 博士, 研究员, 博士生导师, CCF 高级会员, 主要研究领域为计算机控制, 可信软件, 信息物理系统.
董晓刚, 研究员, 主要研究领域为嵌入式高可信软件开发, 软件缺陷检测, 软件智能开发.
杨孟飞, 博士, 研究员, 博士生导师, CCF 会士, 主要研究领域为空间飞行器设计, 控制计算机, 可信软件, 软件智能开发.
刘洋, 硕士, 主要研究领域为软件工程, 自然语言处理.
冀振燕, 博士, 教授, 博士生导师, CCF 高级会员, 主要研究领域为人工智能, 信息安全, 软件工程.