11月20日 （Sessions   1-2，会议室7）

14:00-15:30

主持人：田聪

基于异质图神经网络的大粒度Pull Request描述

自动生成

邝砾，施如意，赵雷浩，张欢，

高洪皓

Petri网的反向展开及其在程序数据竞争检测的

应用

郝宗寅，鲁法明

个体交互行为的平滑干预模型

刘霄，章昭辉，魏子明，王鹏伟

面向AADL系统架构的存储资源约束可调度性

分析方法

陆寅，秦树东，习乐琪，董云卫

面向CPS时空性质验证的混成AADL建模与模型转换方法

陈小颖，祝义，赵宇

15:30-15:42

茶 歇

15:42-17:30

主持人：姜宇

C2P:基于 Pi 演算的协议 C 代码形式化验证方法和工具

张协力，祝跃飞，顾纯祥，陈熹

基于分支调度标记的数据流模型的代码生成方法

苏卓，王东艳，杨镒箫，张明睿，

孙家广

单分支线性约束循环程序的终止性分析

李轶，唐桐，吴文渊，冯勇

基于锁增广分段图的多线程程序死锁检测

鲁法明，郑佳静，包云霞，曾庆田，段华

基于污染变量关系图的Android应用污点分析工具

张捷，田聪，段振华

面向ROS的差分模糊测试方法

王颖，王冰清，关永，李晓娟，王瑞

11月21日（Session   3，会议室7）

11:00-12:30

主持人：田聪

面向数据流的 ROS2 数据分发服务的形式建模与性能分析

芦倩，李晓娟，关永，王瑞，

施智平

支持乱序执行的Raft协议

谷晓松，魏恒峰，乔磊，黄宇

面向 SPARC 处理器架构的操作系统异常管理

形式化验证

马智，乔磊，杨孟飞，李少峰

芯片开发的功能验证形式化方法与应用

姚广宇，张南，田聪，

段振华，刘灵敏，孙风津

基于MSVL的智能合约形式化验证

王小兵，杨潇钰，舒新峰，赵亮

11月21日（Session   4，特丽斯酒店会议厅）

11:00-12:48

主持人：邓玉欣

在Coq中对Verifiable C程序逻辑可靠性证明的模块化重构

王卫兵，万文，曹钦翔

基于Coq的分块矩阵运算的形式化

麻莹莹，马振威，陈钢

以太坊中间语言的可执行语义

韩宁，李希萌，张倩颖，王国辉，施智平，关永

基于活动图与顺序图的自动代码生成及一致性验证

文浩，蒋建民，张仕，洪中

Ptolemy离散事件模型形式化验证方法

陆芝浩，王瑞，孔辉，关永，

施智平

利用形式化方法验证无缓冲区溢出问题的实践与挑战

徐凌云