|
2017年10月21日 |
||
|
上午 7:30 - 8:15 |
注册（长沙延年世纪酒店） |
|
| 上午8:15 - 8:30 | 开幕式（大会议室） | |
| 主持：詹乃军 | ||
| 林惠民:形式化专委与FMAC | ||
| 王戟：SETTA与FMAC组织情况介绍 | ||
| 上午8:30 - 9:30 | 特邀报告（大会议室） | |
| 主持：詹乃军 | ||
| Yu-Fang Chen(Sinica) The Commutative Problem of MapReduce programs | ||
|
|
|
|
|
上午 9:30 - 10:00 |
茶歇/墙贴报告 |
|
| 上午10:00 - 11:40 | FMAC分组（多功厅）：验证算法 | YR-SETTA(多功厅)：Analysus & Verification |
| 主持：宋富 | Session Chair：陈立前 | |
| Xin Li. Reachability Analysis of Conditional Pushdown Systems with Patterns | Taolue Chen, Yan Chen, Anthony W. Lin, Matthew Hague and Zhilin Wu. What's Decidable About String Constraints with ReplaceAll Function? | |
| Yanhuan Fan, Yongming Li and Haiyu Pan. Constraint Reachability Objective in Lattice-valued Game Graph | Jiahong Jiang, Liqian Chen and Ji Wang. Generating Template Inductive Invariants via SMT Optimization | |
| 胡潇洒, 张越龄, 李建文, 蒲戈光 张敏. 基于不可满 足原因的最小纠正集求解 | Zhe Chen. Parametric Runtime Verification is NP- complete and coNP- complete | |
| Yong Li, Lei Song, Yuan Feng and Lijun Zhang. Verify LTL with Fairness Assumptions Efficiently | ||
|
上午 11:40 - 下午1:00 |
午餐 |
|
| 下午1:00 - 2:40 | FMAC 分组:模型检测 | YR-SETTA Session: Probabilistic & Quantum Systems |
| 主持：贺飞 | Session Chair：邓玉欣 | |
| Niu Jun and Wang Wei. Model Checking Interactive Markov Chains against Action-based Regular Specifications | Chao Huang, Xin Chen, Wang Lin, Zhengfeng Yang, Xuandong Li. Probabilistic Safety Verification of Stochastic Hybrid Systems Using Barrier Certificates | |
| Cai Xiaowei and Zhang Min. 自治移动机器人永恒探索算 法的符号化模型检测方法 | Pengfei Yang, David N. Jansen and Lijun Zhang. Distribution-based Bisimulation for Labelled Markov Processes | |
| 喻垚慎, 黄志球, 沈国华 王飞. 基于抽象解释的嵌入式软件 模块化 Cache 行为分析框架 | Andrea Turrini. Model Checking omega-regular Properties for Quantum Markov Chains | |
| Yangjia Li.Termination Analysis for Quantum Programs | ||
|
下午 2:40 - 3:00 |
茶歇/墙贴报告 |
|
| 下午3:00 - 4:40 | 软件学报分组:算法 | YR-SETTA Session: Modeling & Controlling |
| 主持：吴志林 | Session Chair：田聪 | |
| 郑晓琳,邓玉欣,付辰,雷国庆 互模拟准局部验证算法的优 化与实现 | Yi Li, Xiyue Zhang, Yuanyi Ji and Meng Sun. Capturing Stochastic and Real-Time Behavior in Reo Connectors | |
| 汤震浩,李彬,翟娟,赵建华. 自动分析递归数据结构的归 纳性质 | Chao Huang, Xin Chen, Yifan Zhang, Shengchao Qin, Yifeng Zeng and Xuandong Li. Hierarchical Model Predictive Control for Switched Linear Multi- Robot Navigation | |
| 张业迪,宋富. 交替时态逻辑 的语义分析与模型检查 | Liming Li, Zhiping Shi, Yong Guan, Qianying Zhang and Yongdong Li. Formalization of geometric algebra in HOL Light | |
| 李彬,翟娟,汤震浩,汤恩义,赵 建华. 自动合成数组不变式 | Liyun Dai. Feye: A Tool for Identifyin g Semantic Differences Between Versions of Programs | |
| 下午5:00 - 6:15 | 软件学报分组:理论 | 软件学报分组:验证 |
| 主持：李国强 | 主持：张立军 | |
| 张文博,龙环. 向量加法系统 验证问题研究综述 | 王海洋,段振华. APTL 公式的 可满足性检查工 具:APTL2BCG | |
| 朱维军. 拟态自动机 | 李晅松,陶先平,宋巍. 算应用 时空性质的运行时验证 | |
| 乌尼日其其格,李小平,马世 龙,吕江花. 基于类型理论的 领域数据建模及案例研究 | 王小兵,郭文轩. 一种基于消 息传递的 MSVL 通信机制 | |
|
下午 6:20 - 8:00 |
会议宴会 |
|
|
下午 8:20 – 10:00 |
CCF形式化方法专业组会议 |
|
|
|
|
|
|
2017年10月22日 |
||
|
上午 8:30 - 9:30 |
特邀报告（大会议室） |
|
|
主持：傅育熙 |
||
|
Hao Zhong (Shanghai Jiao Tong University) Formalizing hidden program properties |
||
|
上午9:30 - 10:00 |
茶歇/ 贴墙报告 |
|
| 上午10:00 - 11:40 | FMAC 分组:分析与验证 | 软件学报分组:嵌入式系统分析 |
| 主持：孙猛 | 主持:冯新宇 | |
| Shuxian Zhang, Yongwang Zhao, Yan Teng and Feng Zhang. Model-driven Development and Formal Analysis of A GNC Telemetry System | 崔进,段振华,田聪,张南. 一种 中断嵌套系统的建模和分析 方法 | |
| Cao Yan, Huang Zhiqiu, Yu Yaoshen and Xia Yao. Specification and Verification of a Formal Adaptive Role-based Access Control Model for Cyber- Physical Systems | 应云辉,张民. 基于 SMT 的时 钟约束语言 CCSL 的统一形 式化分析方法与工具 | |
| Xinghua Yao, Hengyang Wu and Yixiang Chen. PADS 中迹的刻画以及基 于迹等价的调度分析 | 于广良,杨孟飞. 考虑中断和 上下文切换开销的响应时间 分析 | |
| 孟瑶,李晓娟,关永,王瑞,张 杰. 于 CAN 的机器人关节通 信系统的建模与验证 | ||
|
上午：11:40 – 12:00 |
闭幕式 |
|
点击下载：FMAC 2017 会议册