ChinaSoft 论坛巡礼 | 安全攸关软件的智能化开发方法论坛

2023年CCF中国软件大会（CCF ChinaSoft 2023）由CCF主办，CCF系统软件专委会、形式化方法专委会、软件工程专委会以及复旦大学联合承办，将于2023年12月1-3日在上海国际会议中心举行。

本次大会主题是“智能化软件创新推动数字经济与社会发展”，学术、工业、教育、竞赛等分论坛活动40余场，期待您的参与！

目前大会火热报名中！

CCF ChinaSoft 2023官方首页：

http://chinasoft.ccf.org.cn/

点击文末“阅读原文”或扫描下方二维码进入官方注册通道:

https://conf.ccf.org.cn/chinasoft2023

✦ +

论坛巡礼

论坛名称：安全攸关软件的智能化开发方法论坛

时间: 2023年12月1日（星期五），14:00 – 18:00

地点: 上海国际会议中心，5I会议室

论坛简介：

融合智能化技术的软件开发方法是当前软件工程领域的研究热点和重要发展方向。模型驱动方法已成为国外航空、航天等领域安全攸关软件的主流开发模式，我国航空航天等装备研制领域也正在从传统开发方式向模型驱动方式转变。模型驱动开发方法仍然面临模型构建效率低、代码开发成本高、形式验证难度大、系统验证不充分等挑战。本论坛主题为安全攸关软件的智能化开发和验证方法。将智能化技术与模型驱动相结合，形成“模型驱动+智能增强”的软件开发新模式，创新地解决软件模型构建、安全代码开发、软件验证认证、系统仿真测试等方面的难题，有效解决安全攸关软件开发效率和软件质量提升问题，有望引领新一代安全攸关软件开发的发展方向

日程安排

Schedule

论坛主席

Forum Chairmen

胡春明

北京航空航天大学

博士、教授、博导。现任可信网络计算技术国防重点学科实验室副主任、北京市大数据科学与脑机智能高精尖创新中心副主任，北航软件学院院长。主要从事计算机软件与理论、安全攸关软件开发与测试方法、云计算与大数据、网络化软件开发方法研究工作。曾获国家科学技术发明二等奖1项（排名第2）、中国电子学会科技进步特等奖1项（排名第3）、一等奖1项（排名第3），获第十四届中国青年科技奖，2018年入选科技部中青年科技领军人才，2019年入选中组部万人计划科技创新领军人才。

董威

国防科技大学

国防科技大学计算机学院教授、博士生导师，主要研究方向为高可信软件技术、智能化软件开发方法，中国计算机学会形式化方法专委会秘书长。入选教育部新世纪优秀人才支持计划，曾获中国计算机学会首届NASAC青年软件创新奖、霍英东基金会高校青年教师奖等。先后主持国家自然科学基金重大项目课题、国家863和973课题、国防领域课题十余项，发表学术论文70余篇，出版国家级规划教材两部，相关成果应用于航空航天、装备控制、自主基础软件等关键领域。

葛宁

北京航空航天大学

北京航空航天大学软件学院副教授，博士生导师。2014年博士毕业于法国图卢兹国立综合理工学院，2014-2015年法国CNRS-LAAS博士后，2015-2017在法国IRT-Saint Exupéry工作。主要研究方向为形式化方法。主持国家自然科学基金、国家重点研发计划课题、国防基础加强课题、北航-华为关键软件研究项目等。任中国计算机学会CCF形式化方法、软件工程专委会委员。

论坛嘉宾

Forum Guests

熊英飞

北京大学

2009年从日本东京大学获得博士学位，2009-2011年在加拿大滑铁卢大学工作，2012年加入北京大学，现任新体制长聘副教授、软件研究所副所长、计算机学院院长助理。熊英飞的研究兴趣是程序设计语言和软件工程，特别是程序合成、修复和分析。他提出了理论和方法降低程序编写和缺陷修复的代价。比如，基于差别的双向变换框架是最广泛使用的双向变换框架之一，概率和逻辑结合的程序合成框架玲珑框架将程序修复的正确率从此前不到40%提升到80%以上。他的工作也被工业界采用，比如新一代Linux内核配置项目、燕云DaaS系统、华为公司等。他获得电子学会自然科学一等奖（排名1）、CCF-IEEE CS青年科学家奖、MODELS十年最有影响力论文奖，5次获得ACM SIGSOFT/IEEE TCSE杰出论文奖。他是SATE18的程序委员会联合主席，也在PLDI、ICSE、FSE等会议担任PC。

报告题目：

基于算法模式合成高效程序

报告摘要：

算法优化是程序员的痛点和难点，也是安全攸关软件的主要错误来源之一，自动进行有保障的算法优化有望显著降低安全攸关软件开发成本，提高安全攸关软件质量。传统程序合成主要关注功能正确性，较少对合成程序进行算法优化。优化算法的基本手段是应用人们总结出来的各种算法模式，但直接应用算法模式会有较大挑战。北京大学团队近期针对这个问题开展研究，提出了自动应用分治类和动态规划算法模式的方法。本报告将介绍北京大学在这方面的进展。

赵永望

浙江大学

教授/博士生导师，移动终端安全技术浙江省工程研究中心主任，工信部重大专项首席科学家，CCF杰出会员。主要研究方向为系统安全、形式化验证、编程语言、嵌入式操作系统等，主持和参与国家重点研发计划、国家自然基金重点项目、工信部重大专项、载人航天工程重点项目等三十余项，获省部级科技进步一等奖2项，相关成果发表在ACM TOPLAS、IEEE TDSC等期刊和CAV、FM、TACAS等会议上。

报告题目：

安全攸关软件形式化验证工具的一些探索

报告摘要：

安全攸关软件是一类其错误/故障会导致系统失效，从而引起重大生命、财产损失的软件。形式化验证已成为工业界保证安全攸关软件正确性和安全性的主要手段之一，但是，目前业界的形式化验证工具存在技术门槛高、易用性低、适用面有限等不足，本报告主要介绍我们研发的一系列形式化验证工具，包括定理证明云平台、源码自动化验证工具、符合CC的形式化框架等，并介绍这些工具的实际应用与不足，进一步讨论探索形式化验证工具研发的一些观点。

陈振邦

国防科技大学

国防科技大学计算机学院教授、博士生导师。主要研究方向为程序分析、形式化方法及其在不同背景下的应用。近年来主要围绕符号执行相关的理论、技术和应用开展研究，成果发表在ICSE、FSE、ISSTA、ASE、FM、TCS等重要国际会议或期刊上，获ACM SIGSOFT杰出论文奖2次。获国家科技进步二等奖1项、省部级科技进步二等奖2项，获NASAC青年软件创新奖。

报告题目：

面向符号执行的约束求解

报告摘要：

符号执行是一种基于约束求解的通用程序分析技术，而约束求解也是符号执行面临的主要挑战之一。本报告将汇报近期在面向符号执行的约束求解方面的工作，希望从两个方面提升符号执行的分析效率。一方面我们基于机器学习方法提升符号执行背景下约束求解的智能化程度；另一方面我们希望把约束求解这一人工智能领域的经典问题的求解过程打开，为符号执行提供更多的帮助。