形式化方法与应用论坛
2022年11月25日（8:30–12:30，13:30–17:30）
论坛简介
形式化方法与应用论坛是依托中国计算机学会形式化方法专委，在中国软件大会上持续组织的一个重要活动，是促进形式化方法理论及其工业应用的学术交流与技术发展研讨的一个重要平台。 论坛组织过程包括如下几个阶段：1) 论文征集与评审：论坛共征集到41篇学术论文，每篇论文至少经2-3位评审人进行2轮评审并打分，选出了10篇优秀论文，论文名单见日程安排表。2) 论文汇报交流：编委会选出10篇优秀论文到CCF ChinaSoft2022的形式化方法与应用论坛进行汇报交流。3）论文修改与发表：根据会场专家提问和评审专家意见，对论文进行修改后，论文修改达标后将在软件学报专刊发表。这10篇论文涉及软件形式化建模理论、形式化验证方法、智能形式化方法、软件形式化开发工具及应用等研究成果。
论坛日程
| 时间 | 报告题目 | 讲者 |
|---|---|---|
| 第一单元主持人：董云卫（西北工业大学，教授） | ||
| 08:30-09:15 | 自动驾驶交叉路口测试场景建模及验证方法 | 夏春艳, 黄松, 郑长友, 张清睿, 王宇, 魏瑀皓 |
| 09:15-10:00 | 基于约束依赖图的并发程序模型检测工具 | 苏杰, 杨祖超, 田聪, 段振华 |
| 10:00-10:40 | 具有安全保证的神经网络控制器生成方法 | 赵庆晔, 王豫, 李宣东 |
| 10:40-11:20 | 一种基于LLVMPass的复杂嵌套循环自动并行化框架 | 马春燕, 吕炳旭, 叶许姣, 张雨 |
| 11:20-12:00 | 智能规划中面向简单偏好的高效求解方法 | 陆旭, 于斌, 段振华, 王德奎, 陈矗, 崔进 |
| 第二单元主持人：刘关俊（同济大学，教授） | ||
| 13:30-14:15 | 面向未解释程序的合作验证方法 | 杜一德, 洪伟疆, 陈振邦, 王戟 |
| 14:15-15:00 | 基于SMT的区域控制器同步反应式模型的形式化验证 | 李腾飞, 孙军峰, 吕新军, 陈祥, 刘静, 孙海英, 何积丰 |
| 15:00-15:40 | 可信执行环境的运行时安全形式化验证技术 | 潘少平, 常瑞, 张子君, 赵永望 |
| 15:40-16:20 | 一种目标导向的多线程程序UAF漏洞检测方法 | 鲁法明, 唐梦凡, 包云霞, 曾庆田, 李彦成 |
| 16:20-17:00 | 前馈神经网络和循环神经网络的鲁棒性验证综述 | 刘颖, 杨鹏飞, 张立军, 吴志林, 冯元 |
论坛主席
1.论坛主席：董云卫（西北工业大学）
简介：
西北工业大学计算机学院教授，博士生导师，西工大智能嵌入式软件研究中心副主任，IEEE可靠性协会西安分会主席。IEEE高级会员，中国计算机学会杰出会员、中国计算机学会形式化专委会常委、嵌入式系统专委会常委、软件工程专委会会员。2000年获首届“陕西省十大软件行业杰出青年”，2001年获首届“中国软件行业杰出青年”提名。长期从事模型驱动的软件开发方法、软件智能合成理论与方法、智能系统测试等技术的研究，发表论文共计100余篇，并拥有15项中国发明专利。
2.论坛主席：刘关俊（同济大学）
简介：
同济大学计算机科学系教授、博士生导师。中国计算机学会形式化方法专委会与软件工程专委会执行委员，IEEE高级会员。曾先后于新加坡科技设计大学、柏林洪堡大学（德国洪堡基金资助）开展博士后研究工作。主要从事模型检测、Petri网理论、物理信息系统、工作流系统、基于强化学习与软件定义的无人机协同系统、以及基于深度学习的网络交易欺诈检测等方面的研究。在国内外期刊与会议上发表学术论文100余篇，出版学术专著2本。主持国家自然科学基金青年基金项目1项、面上项目2项、重点项目子课题1项。作为主要完成人获国家科技进步二等奖、电子学会自然科学一等奖、自动化学会自然科学一等奖、吴文俊人工智能技术发明一等奖各1项。
3.论坛主席：毛晓光（国防科技大学）
简介：
国防科技大学计算机学院教授，博士生导师，软件工程学科带头人，教育部计算机类专业教学指导委员会委员，中国高校计算机教育MOOC联盟理事，首批国家级一流本科课程负责人，享受国务院政府特殊津贴。从事软件工程领域的科学研究和教育教学工作。曾获国家级教学成果二等奖2项、省部级教学成果一等奖1项，省部级科技进步一等奖2项、二等奖3项。在《中国科学》、《软件学报》、TOSEM、TSE、POPL、ICSE、FSE、ASE等会议刊物上发表论文百余篇，出版教材8部。CCF软件工程专委会常务委员、形式化方法专委会委员、开源发展委员会执行委员。