专刊论坛

形式化方法与应用论坛

2023年12月1日(星期五),8:30 – 18:00

上海国际会议中心,3B会议室



论坛简介

软件发展的核心问题之一是如何保证软件系统安全可靠。随着形式验证技术(如定理证明、模型检验等)的发展,形式化方法在提高软件可靠性方面己显示出无可取代的潜力。各个著名的研究机构都投入了大量人力和物力从事这方面的研究。例如,美国宇航局(NASA)拥有一支庞大的形式化方法研究团队,他们在保证美国航天器控制软件正确性方面发挥了巨大作用,在美国研发“好奇号”火星探测器时,为了提高控制软件的可靠性和生产率,广泛使用了形式化方法。在新兴领域,如区块链及人工智能等领域,形式化方法也逐步应用适配,提升系统的整体安全可控。

《形式化方法与应用》论坛主要关注形式化方法基础理论、技术、支撑工具以及领域应用。今年的《形式化方法与应用》专刊论坛共收到稿件44份,经过两轮审稿,最终15篇论文通过评审被邀请到论坛汇报。另外,本论坛还邀请了产业界的专家来分享他们最新的研究成果及见解。

论坛日程

时间 主题 嘉宾/论文作者
上午
08:30-08:40 开场致词 论坛主席
08:40-09:00 论文报告:完备神经网络验证加速技术综述 刘宗鑫,杨鹏飞,张立军,吴志林,黄小炜
09:00-09:20 论文报告:基于PAC学习的组合式概率障碍证书生成方法 杨紫萱,曾霞,任勐鑫,王建林,曾振柄,杨争峰
09:20-09:40 论文报告:VDMBS:一种基于形式化方法的区块链系统漏洞检测模型 陈锦富,冯乔伟,蔡赛华,施登洲, Rexford Nii Ayitey Sosu
09:40-09:50 合影
09:50-10:10 茶歇
10:10-10:30 论文报告:微内核操作系统互斥量模块功能正确性的形式化验证 张林雁,李希萌,施智平,关永,曹钦翔,张倩颖
10:30-10:50 论文报告:命令式动态规划类算法程序推导及机械化验证 左正康,孙欢,王昌晶,游珍,黄箐,王唱唱
10:50-11:10 论文报告:基于交互式定理证明的并发程序验证工作综述 王中烨,吴姝姝,曹钦翔
11:10-11:30 论文报告:Trie+结构函数式建模、机械化验证及其应用 左正康,柯雨含,黄箐,王玥坤,曾志城,王昌晶
11:30-11:50 论文报告:基于DH标定的机器人正向运动学形式化验证 谢果君,杨焕焕,石正璞,陈钢
下午
14:00-14:30 邀请报告:形式化方法在自动驾驶软件设计中的应用 科大国创
14:30-14:50 论文报告:基于AADL的混合关键系统随机错误与突发错误安全性分析 魏晓敏,董云卫,孙聪,李兴华,马建峰
14:50-15:10 论文报告:Büchi自动机确定化分析工具 马润哲,田聪,王文胜,段振华
15:10-15:30 论文报告:并发对象强可线性化性质的检测和验证研究 王超,贾巧雯,吕毅,吴鹏
15:30-16:00 茶歇
16:00-16:20 论文报告:关于安全案例论证构建的综述 陈泽众,邓玉欣
16:20-16:40 论文报告:舰载机弹药保障作业调度的形式化建模与验证 金钊,金璐,张博闻,吴庆顺,冯朔,李冠峰,徐明亮
16:40-17:00 论文报告:基于MTRDL的自动飞行系统模式需求建模与验证方法 徐恒,黄志球,胡军,陶传奇,王金永,石帆
17:00-17:20 论文报告:基于优先级时间Petri网的实时嵌入式多核系统分析 张凯文,刘关俊,孙彦韬,李晓锋,关健,解毅,顾斌

论坛主席





1.论坛主席:曹钦翔(上海交通大学)

简介: 上海交通大学副教授,2013年本科毕业于北京大学,2018年在普林斯顿大学获得博士学位,2018年至今,其担任上海交通大学助理教授、副教授,曾获上海浦江人才计划资助。曹钦翔长期从事基于定理证明的程序验证与程序逻辑研究,论文主要发表在POPL、OOPSLA、JAR等国际著名会议或期刊,其代表性工作是其领衔开发的VST程序验证工具系列。在此基础上,曹钦翔还参与撰写了Coq定理证明知名教材《Software Foundations》的第五卷。





2.论坛主席:宋富(中国科学院软件研究所)

简介: 中国科学院软件研究所研究员,主要研究系统与软件安全验证和测试技术、及相关逻辑和自动机理论。宋富于2013年获巴黎狄德罗大学博士学位,2013年--2016年曾在华东师范大学担任讲师和副研究员,2016年--2023年担任上海科技大学助理教授、常任副教授,研究员,博士生导师。主持和参与多项国家自然科学基金委青年、面上和重点项目,曾获上海市浦江人才和上海市晨光学者人才计划资助、2021年秋季亚马逊研究奖、入选中国电子学会2023网络空间安全优秀论文,已在国际著名会议或期刊(如IEEE S&P、USENIX Security、NDSS、POPL、OOPSLA、CAV、ESEC/FSE、ICSE、ASE、ISSTA、FM、ACM TOSEM、IEEE TSE、IEEE TDSC、I&C)发表80多篇论文。





3.论坛主席:詹乃军(中国科学院软件研究所)

简介: 中科院软件所研究员,中科院特聘研究员,中国科学院大学岗位教授,计算机科学国家重点实验室执行主任,国家杰出青年科学基金获得者。分别在南京大学数学系(1989-1993)和南京大学计算机系(1993-1996)获得学士和硕士学位,在中国科学院软件研究所获得博士学位(1997-2000)。研究方向包括:实时、嵌入式和混成系统设计理论以及程序理论等。任《Journal of Automated Reasoning》、《Formal Aspects of Computing》、《J. of Logical and Algebraic Methods in Programming》、《Research Direction: Cyber-Physical Systems》、《软件学报》、《计算机研究与发展》《电子学报》、《前瞻科技》等期刊编委,国际会议MEMOCODE和SETTA的指导委员会委员,多个国际会议程序委员会共同主席(如形式化方法旗舰会议FM 2021)和著名国际会议程序委员会委员(如CAV、RTSS、HSCC、ICCPS、EMSOFT等);在著名国际会议和杂志发表论文100多篇,出版专著2部,编著4部。