|
2019年11月30日 |
|||
|
上午 7:30 - 8:15 |
会议注册（上海 华东师范大学 科学会堂） |
||
| 上午8:15 - 8:30 | 李志斌副校长：开幕词 | ||
| 主持：詹乃军 | |||
| 林惠民院士:形式化专委会与FMAC | |||
| 傅育熙：SETTA与FMAC组织情况介绍 | |||
| 上午8:30 - 9:30 | 特邀报告（科学会堂） | ||
| 主持：詹乃军 | |||
| 关楠. Scheduling and Analysis of Parallel Real-Time Software | |||
|
|
|
||
|
上午 9:30 - 10:00 |
合影/茶歇（数学馆） |
||
| 上午10:00 - 12:00 | FMAC(session1) (科学会堂) Probabilistic and stochastic systems | 软件学报专刊 (数学馆113报告厅) 新兴系统的形式语言、模型检测与测试 | YR-FMAC (数学馆201报告厅) Stochastic, Hybrid/Real-time Systems Verification and Modelling |
| 主持：刘万伟 | 主持：刘志明 | 主持：薛白 | |
| Xiaoyong Xue and Meng Sun. Probabilistic Extension of Mediator | 李小平,乌尼日其其格,马世龙,吕江花. 高阶类型化模型驱动的可验证应用系统体系结构建模及案例 | Zhengfeng Yang. Safety Verification of Nonlinear Hybrid Systems Based on Bilinear Programming | |
| Rongfei Xu, Li Zhang and Ning Ge.Probabilistic Schedulability Analysis of Real-time Tasks with Precedence Constraints | 李璜华,李凌,赵宇,殷树娟,王生原,李翔宇. 一种可重构包解析器硬件配置描述语言的设计及其编译结构 | Hui Kong. 混杂系统的不变式生成方法 | |
| An Dongdong. A Modeling Framework for Automatic Quantitative Analysis of Cyber-Physical-Social Systems | 谭锦豪,李国强. 基本并行进程活性的限界模型检测 | Meilun Li.Reachability Estimation of Stochastic Dynamical Systems by Semi-definite Programming | |
| Haiyang Hu, Jiawei Yu, Zhongjin Li, Jie Chen and Hua Hu. Modeling and Analysis of Cyber-Physical System Based on Object-Oriented Generalized Stochastic Petri Net | 宋巍,李晅松,肖芳雄. 面向实例迁移的服务组合回归测试 | Min Zhang.Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint | |
| 陆超逸,聂长海,张成志. 一种验证分布式协议活性属性容错机制的模型检测方法 | 张时雨. 面向智能家居物联网的自然语言到LTL规约自动生成 | ||
| Lingtai Wang. The Opacity of Real-time Automata | |||
|
上午 12:00 - 下午1:30 |
午餐（华东师范大学河东餐厅三楼） |
||
| 下午1:30 - 3:30 | FMAC(session2)(科学会堂)Real-time systems | FMAC (session3) (数学馆113报告厅)Algorithms | YR-FMAC(数学馆201报告厅)Program Analysis and Verification |
| 主持：赵建华 | 主持：李国强 | 主持：陈立前 | |
| Xiangyu Luo, Sen Liang, Zuxi Chen and Fan Yang. Counterexample Generation for Real-Time Branching Temporal Logic | Feifan Xu, Fei He, Enze Xie and Liang Li. Fast OBDD Reordering via Message Passing Neural Network | Yongwang Zhao. 一种并发反应式系统组合验证的方法、实现及应用 | |
| Jin Lv, Yongxin Zhao, Xi Wu, Yongjian Li and Qiang Wang . Formal Analysis of TSN Scheduler for Real-Time Communications | Junyan Qian, Yong Cai and Haiyu Pan. Approximate Safety Properties in Metric Transition Systems | Bohua Zan. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic | |
| Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Learning One-Clock Timed Automata | Shenghao Yuan, Zhibin Yang, Bolin Zhang, Yong Zhou, Lei Xue, Jean-Paul Bodeveix and Mamoun Filali 基于同步语言的多任务Ada代码生成方法 | 尹良泽. Parallel Refinement for Multi-threaded Program Verification | |
| Cong Chen, Zhong Hong, Yangyang Chen, Shi Zhang and Jianmin Jiang 移动系统的实时调度与可调度性分析 | 张旭初，石海鹤。 多序列比对算法构件的设计与实现 | 刘嘉祥. Verifying Arithmetic in Cryptographic C Programs | |
| Zhilin Wu. Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps | |||
| 李建文. An Overview of Complementary Approximate Reachability | |||
|
下午 3:30 - 4:00 |
茶歇/墙贴报告 |
||
|
下午 4:00 - 5:30 |
赵建华. 交互式代码形式验证 (Tutorial，科学会堂) |
||
|
下午 6:00 |
会议晚宴(环球港三楼顺风港湾) |
||
|
下午 8:00 - 10:00 |
CCF 形式化方法专委会会议 |
||
|
2019年12月1日 |
|||
|
上午 8:30 - 9:30 |
特邀报告 (科学会堂) |
||
|
主持：胡振江 |
|||
|
董劲松. Trusted Decision Making and Dependable Intelligence |
|||
|
上午 9:30 - 10:00 |
茶歇(科学会堂) |
||
| 上午 10:00 - 12:00 | FMAC (session4) (科学会堂) Model verification and analysis | FMAC (session5) (数学馆 113 报告厅) Verification and proving | 软件学报专刊 (数学馆 201 报告厅)新兴系统的形式规约与定理证明 |
| 主持：董云卫 | 主持：贺飞 | 主持:冯新宇 | |
| Jiaqi Yin, Huibiao Zhu, Yuan Fei, Qiwen Xu and Yang Tao. Formal Modelling and Verification of the RTPS StatefulWriter Module | Leifeng He and Guanjun Liu. Verifying Computation Tree Logic of Knowledge via the Similar Reachability Graphs of Knowledge- oriented Petri Nets | 李亚男,邓玉欣. 基于 Coq 的 Paxos 形式化建模与验证 | |
| Pei Tang, Yunwei Dong and Xiaoming Wei. Schedulability analysis based on IO constrained AADL model | Bohua Zhan. holpy: Interactive Theorem Proving in Python | 姜菁菁,乔磊,杨孟飞,杨桦,刘波. 基于Coq的操作系统任务管理需求层建模及验证 | |
| Bolin Zhang, Zhibin Yang, Zhou Yong, Yanyan Ma, Zhiqiu Huang and Lie Xue。 一种面向航天应用的 AADL 模型组合验证方法 | Xiaobing Wang, Yanmei Wang, Liang Zhao and Xinfeng Shu. Implementation and Application of a Runtime Verification Method Based on Three-Valued PPTL | 李少峰,乔磊,杨孟飞,杨桦,王泉,杨鹏飞. 基于归纳演绎的内存状态验证 | |
| Jincao Feng, Jiayi Zhu, Yihao Huang, Hanyue Zheng, Shang Wang, Xiangrong Xu, Weikai Miao and Geguang Pu。 轨道交通控制软件需求模型的量纲分析方法 | 郑小宇, 刘冬梅, 杜益 宁, 周子健, 邱玫 媚 ，朱鸿。 模式驱动的系统安全性设计的验证 | 易星辰,魏恒峰,黄宇,乔磊,吕建. PaxosStore 中共识算法 TPaxos 的推导、规约与精化 | |
| 陈钢,崔敏,陈曦,马振威,汪一飞. 形式化工程数学和下一代人工智能 | |||
|
上午 12:00 |
午餐(华东师范大学河东餐厅三楼) |
||
|
下午 1:30 - 4:35 |
工业报告 (科学会堂) |
||
|
下午 1:30 - 1:35 |
开场致辞 主持:蒲戈光 |
||
|
下午 1:35 - 2:05 |
代声馨，刘洪宇 (华为) 形式化方法工程落地的长期演进思考 |
||
|
下午 2:05 - 2:35 |
陈晓轩 (卡斯柯) 形式化开发在轨交信号系统的应用与展望 |
||
|
下午 2:35 - 3:05 |
马恩 (中国商发) 商用航空发动机软件工程考虑 |
||
|
下午 3:05 - 3:35 |
李亚晖 (航空工业计算所) 机载信息处理系统 MBSE 解决方案 |
||
|
下午 3:35 - 4:05 |
李健 (电科三十二所) 高可靠嵌入式实时操作系统实践及展望 |
||
|
下午 4:05 - 4:35 |
周正辉 (上海控安) 嵌入式系统单元测试工具 |
||
|
下午 4:35 - 4:50 |
FMAC 最佳论文奖颁奖及闭幕式 (科学会堂) |
||