2023年11月11日下午，“大模型背景下基础软件及工具链的形式化验证方法”技术论坛在苏州高研院唯真楼4楼第一会议室举行，会议由中国计算机学会（CCF）主办，CCF YOCSEF苏州学术委员会承办，高研院协办。YOCSEF总部联系AC鄢兴雨，现任CCF苏州YOCSEF主席史国良，副主席许佳捷，学术秘书叶雅梅，AC委员徐峰磊、孙高飞，中国航天五院502所研究员乔磊，浙江大学研究员姚培森，华为苏州研究所高级工程师钱忆等20余人参加本次会议。本次论坛执行主席是YOCSEF苏州AC委员王超和薛吟兴。
论坛的引导发言环节由王超主持，他介绍了论坛的背景和参会的嘉宾，作了开场致辞。
来自中国航天五院502所研究员乔磊做了题为“航天器操作系统的研究与实践”的精彩报告。该发言从航天器计算机特征出发，介绍了研究所研制的SpaceOS I、SpaceOS II和SpaceOS III等航天操作系统及其相关典型应用，如载人航天、深空探测和通信等。乔磊研究员还分享了航天器操作系统的设计，如操作系统研制流程和不同的功能组成等，介绍了操作系统的任务调度策略，并在最后给出了研究所相关研究的总结。
浙江大学研究员姚培森则从软件质量保障的角度作了主题为“基于符号抽象的程序分析”的报告。报告点出程序分析是保障软件质量的重要手段，而抽象解释理论是静态程序分析的核心理论，姚培森介绍了基于抽象解释的程序分析和验证工具，符号抽象框架等。报告还分享了近期关于计算最佳多面体抽象的研究工作，提出尝试采样更极端的高质量解、借助最佳区间抽象寻找“极端解”的想法。
华为苏州研究所高级工程师钱忆从智能驾驶供应链出发，作了主题为“智能驾驶大规模仿真”的报告。报告介绍了测试评价工具链、智能大规模仿真的组成，分享了华为团队近些年的研究进度和未来研究目标：构建全球领先的大规模仿真数据集，评测准确性进一步提升，最终实现完全自动化。
引导发言结束后，参会嘉宾到唯真楼一楼进行合影留念。
论坛的思辨环节由薛吟兴主持，围绕论坛主题，提出三个议题，参会专家从不同角度出发，对三个议题进行思辨研讨，现场讨论气氛热烈、学术氛围浓厚。针对第一个议题：国产基础软件的验证，包括航天操作系统软件等，最大的困境是卡脖子技术问题还是生态问题?参会专家认为技术和生态都有，可能更为突出的是生态问题。主席史国良提出生态问题涉及到三个方面：第一，涉密之后怎么形成生态？第二，商业竞争不利于生态发展该怎么解决？第三，学生就业与生态相关，该如何既保证就业又构建自主可控的生态？。专家钱忆认为生态问题应奉行政府主导推行，企业优先使用，学生再学习的原则，政府主导效率更高。
针对第二个议题：国产基础软件，在LLM蓬勃发展的趋势下，在Langchain等技术背景下，开发和维护过程中有哪些新的挑战？参会专家从多种角度出发，提出大语言模型目前面临的可靠性、泛化性、可解释性及人才协同工作等挑战。
针对第三个议题：基础软件的形式化验证方面，大语言模型的出现是可以帮助形式化验证的效率和准确性，还是更多会带来一些新的安全挑战（例如prompt injection攻击）？专家鄢兴雨表示，可以先生成更容易验证的代码，再根据每个模块生成更有效率但是逻辑相同的代码。对于开源大模型可以找一个基座，再拿出绝对安全的部分代码对它进行相应的规划和训练，这样能有利于解决大模型存在的安全问题。
最后薛吟兴对思辨环节的议题做了相关的总结发言，论坛在轻松愉快的知识分享与交流中结束。
