FMAC2018会议程序手册-华东师范大学

1、FMAC 2018第三届全国形式化方法与应用会议The 3rd National Conference on Formal Methods andApplications2018 年 11月 3 日 4 日，中国重庆会议程序手册会议地点：重庆市北碚区西南大学桂园宾馆会议网址： 第三届全国形式化方法与应用会议（FMAC 2018 ）会议介绍形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已延伸成为计算思维的重要载体。中国计算机学会形式化方法专业委员会成立于 2015 年 11 月，旨在立足于形式化方法核心内容，深化拓展形

2、式化方法与相关领域的交叉，加强学术界与工业界合作，在科学研究、人才培养、国际交流、应用实践等方面努力开展卓有成效的工作，促进形式化方法在中国的发展。第三届全国形式化方法与应用会议（FMAC 2018）由中国计算机学会主办，形式化方法专业委员会和西南大学、华东师范大学承办，将于 2018 年 11 月 3 日至 4 日在重庆西南大学举行。大会将设置特邀报告、论文报告、专题论坛、青年学者论坛、张贴报告、系统展示等多种学术交流形式，会议还将与软件学报等合作组织专题特约报告，为与会代表提供丰富的交流平台。会议特别欢迎形式化方法与理论计算机科学、软件工程、系统软件、嵌入式系统、网络与信息安全、人工智能等

3、学科和领域交叉结合的研究成果和论文。1第三届全国形式化方法与应用会议（FMAC 2018 ）会议组织大会主席程序委员会主席程序委员会刘志明， 西南大学朱惠彪， 华东师范大学庞军 ，卢森堡大学曹永知 ，北京大学陈铭松 ，华东师范大学邓玉欣， 华东师范大学董威，国防科技大学董云卫 ，西北工业大学冯新宇 ，南京大学关楠，香港理工大学贺飞，清华大学孔维强 ，大连理工大学李国强， 上海交通大学李建文， 爱荷华州立大学李晓红， 天津大学李宣东 ，南京大学佘志坤 ，北京航空航天大学宋富，上海科技大学孙猛，北京大学田聪，西安电子科技大学王戟，国防科技大学王林章 ，南京大学魏欧，南京航空航天学吴尽昭 ，广西民族

4、大学吴志林 ，中国科学院软件研究所2第三届全国形式化方法与应用会议（FMAC 2018 ）工业应用程序委员会主席工业应用程序委员会杨红丽 ，北京工业大学詹乃军 ，中国科学院软件研究所张辰一 ，暨南大学张广泉 ，苏州大学张苗苗 ，同济大学张立军 ，中国科学院软件研究所赵恒军 ，西南大学赵永望 ，北京航空航天大学顾斌， 航天科技集团王戟， 国防科技大学刘志明， 西南大学刘洪宇， 华为技术有限公司陈睿， 北京轩宇信息技术有限公司郭宇， 安比（ SECBIT）实验室鲍敏祺， Synopsys组织委员会主席刘波， 西南大学组织委员会代立云， 西南大学梁华珍， 西南大学王庆， 西南大学王勤， 西南大学赵恒

5、军， 西南大学曾霞， 西南大学曹雪莲， 西南大学张婷婷， 西南大学张煜堃， 西南大学宣传主席李国强， 上海交通大学张海涛， 兰州大学3第三届全国形式化方法与应用会议（FMAC 2018 ）主办单位中国计算机学会承办单位形式化方法专委会西南大学华东师范大学4第三届全国形式化方法与应用会议（FMAC 2018 ）会议程序会议地点：西南大学桂园宾馆丹桂楼2:00pm-5:30pm7:00pm-9:00pm8:00am-8:30am8:30am-9:00am9:00am-10:00am10:00am-10:30am2018年11月2日注册（西南大学桂园宾馆丹桂楼大厅）注册（西南大学桂园宾馆丹桂楼大厅）

6、2018年11月3日注册（西南大学桂园宾馆丹桂楼大厅）开幕式（ 3楼 10会议室）主持：詹乃军、专委主任讲话、西南大学计信院领导致欢迎词特邀报告（主持：王戟）Zhenjiang Hu (National Institute of Informatics/University of Tokyo)Verification of Roundtrip Property in BidirectionalProgramming茶歇 / 墙贴报告10:30am-12:00amFMAC分组（ 3楼9会议室）：验证算法主持：朱惠彪Chi Hu, Wei Dong, Yonghui Yang, Hao Shi,

7、Ge Zhou . ROS-based Runtime Verification on Hierarchical Properties of Robot SwarmDehui Du, KaiqiangJiang, Xin Bai.DAL-SMC:Distributed StatisticalModel Checking with Abstraction and LearningXi Deng, Yuxin Deng.Qsimulation:一个量子计算模拟器工具YR-FMAC分组（ 3楼 2会议室）：Program Analysis andVerification ISession Chair

8、： Zhenbang ChenJiangchao Liu,Liqian ChenXavier Rival. AutomaticVerification of EmbeddedSystem Code ManipulatingDynamic Structures Stored inContiguous RegionsFengmin Zhu, Fei He. ConflictResolution for Structured Merge via Version SpaceAlgebraTaolue Chen, Jinlong He, FuSong, Guozhen Wang, ZhilinWu, J

9、un Yan. Android StackMachineNa Yu, Rui Chen, Chunpeng Jia. Improved modularabstract interpretation for interrupt-driven program12:00am-1:30pm合影, 午餐5第三届全国形式化方法与应用会议（FMAC分组（ 3楼9会议室）：程序分析主持：张辰一Ling Li, Yuanke Gan, ShuShang, Shengyuan Wang.AFormally Verified Parserfor the Lustre* Language1:30pm-3:00pmQi

10、 Zhang, Yi Li, MengSun .AutomaticGeneration of SystemCCode from Mediator贾春鹏 ,余娜,车小鹏 ,陈睿.航天嵌入式软件数组越界检测方法研究FMAC 2018 ）YR-FMAC分组（ 3楼 2会议室）：Real-Time Systems Session Chair ： Lei Bu Lingtai Wang, Naijun Zhan, Jie An. The Opacity of Real-time AutomataBingqing Xu ,Qin Li. A Decision-making Model for Autono

11、mous Cars Based on Local Traffic and EstimationKeyin Li. A Unified Framework for Verification of Real-Time SystemsJingran Xu. Formalization of perturbed Kepler problem based on geometric algebra theory3:00pm-3:30pm3:30pm-5:00pm5:00pm-6:30pm茶歇 / 墙贴报告FMAC分组 (3 楼 9会议室 ) ：YR-FMAC分组 (3 楼 2会议室 ) ：Program

12、Analysis and合成Verification II主持：张苗苗Session Chair ：Zhiling WuHao Shi, Rui Li, Wanwei Liu,Yuan Zhuang, Dachuan Shen,Lei Bu. Concurrent CodeWei Dong, Ge Zhou. IterativeSynthesis By StatisticalController Synthesis forModel Checking andMulti-Robot SystemIntelligent SearchLiyun Dai, Bo Liu, ZhimingPengfei

13、 Gao, Jun Zhang, FuSong, Chao Wang. VerifyingLiu, Taolue Chen. Parameterand Quantifying Side-ChannelSynthesis Problems forResistance of Masked SoftwareParametric Timed AutomataImplementationsJiaqi Qian, Min Zhang, YiWang. KupC: A FormalZhiwu Xu, Xiongya Hu, ChengVerification Framework forDynamic Sof

14、tware Updating ofWen, Shengchao Qin.C ProgramsExtracting Automata fromBanghu Yin, Liqian Chen,Neural Networks Using ActiveJiangchao Liu, Ji Wang,LearningPatrick Cousot. ProgramVerification Based onIterative Abstract TestingPanel Session(3楼 10会议室 ):Formal Methods in Industry Applications主持：刘志明讨论嘉宾：顾斌

15、，叶宏，刘洪宇，郭宇，鲍敏祺顾斌（航天科技集团），形式化方法在航天的应用实践与思考刘洪宇（华为技术有限公司），机会与挑战 ICT 全栈产品场景下的形式化验证郭宇（安比（ SECBIT ）实验室），智能合约的安全问题与形式化验证6第三届全国形式化方法与应用会议（FMAC 2018 ）鲍敏祺（Synopsys）， VC Formal概述6:30pm-8:00pm会议晚宴8:20pm-10:00pmCCF 形式化方法专业组会议（3 楼 10 会议室）7第三届全国形式化方法与应用会议（FMAC 2018 ）8:30am-9:00am9:00am-10:00am10:00am-10:30am10:30a

16、m-12:00am12:00am-1:30pm2018年11月4日注册（西南大学桂园宾馆丹桂楼大厅）特邀报告（主持：庞军）Xinyu Feng(Nanjing University)并发 C 程序编译器验证初探茶歇 / 墙贴报告软件学报专刊分组（3楼 2会议FMAC分组（ 3楼9会议室）：室）：建模程序分析与验证主持：邓玉欣主持：贺飞杨志斌,袁胜浩 ,谢健,周勇,陈哲,Wen Su . Modeling of薛垒 ,BODEVEIXJean-Timing Constraints inPaul,FILALIMamoun. 一种基于Hybrid Systems UsingOCAML的同步语言多线程

17、代码自动Event-B生成工具Yihao Huang, JincaoFeng, Hanyue Zheng,Weikai Miao, Geguang Pu.康跃馨 , 甘元科 , 王生原 . 同步数A Formal Engineering据流语言可信编译器 V élus与method for theL2C 的分析与比较Requirements Modeling ofAirborne EmbeddedControl SoftwareYilong Yang, XiaoshanLi, Zhiming Liu, Wei Ke,李轶,蔡天训 , 吴文渊 , 冯勇.基于Quan Zu, Xiaoh

18、ong Chen.SVM 的多项式循环程序秩函数探Automated Prototype测Generation from FormalRequirements Model午餐1:30pm-3:00pmFMAC分组（ 3楼9会议室）：逻辑与分析主持：董威宋佳雯, 肖美华, 王西忠, 杨科 , 钟小妹 . 基于事件逻辑的 PUF 相关认证协议安全性分析Ximing Wen, LiangdaFang, Quan Yu, LiangChang, Ju Wang.Knowledge Forgetting inMulti-Agent Modal LogicSystem KnYR-FMAC分组 (3 楼 2

19、会议室 ) ：Model-based System DesignSession Chair： Min ZhangHaifeng Gu, Jianning Zhang, Mingsong Chen, Fei Xie. Specification-Driven Automated Conformance Checking for Virtual Prototype and Post-Silicon DesignsChengwei Liu, Zhibin Yang, Tao Yue, Yong Zhou, Zhiqiu Huang. Automated Derivation of AADL Mode

20、ls from Requirements in Restricted Natural LanguageYi Li. Component-based Formal Engineering in Mediator8第三届全国形式化方法与应用会议（FMAC 2018 ）何娟娟 ,刘冬梅 ,朱鸿 .面向Xiyue Zhang. Modeling andWeb 服务测试的单线执行序列生Verification of Component成方法Connectors3:00pm-3:30pm3:30pm-5:00pm茶歇 / 墙贴报告软件学报专刊分组 (3 楼 9会议软件学报专刊分组（ 3楼2会议室 ) ：室

21、）：系统建模与分析算法主持：陈立前主持：张立军张锦坤,杨孟飞 ,乔磊,杨桦,刘安杰 , 张苗苗 . 基于实时自动机的波 . 基于有限状态机的操作系统连续时段演算的验证需求层形式化验证杨康, 王瑞, 关永, 李晓娟 ,施智丁如江 , 李国强 . 非交互式 Petri平 , 宋晓宇 . 具有多传感器的 CPS网可覆盖性验证的高效实现系统的攻击检测付春艳 , 郑扣根 . 安全 ad hoc 路朱凯 , 毋国庆 , 吴理华 . 有关时间自动机重置的若干问题的计算复由协议 SRP的建模与分析杂性罗晨霞 ,王瑞 ,关永 ,李晓娟 ,施智乌尼日其其格 , 李小平 , 马世龙 , 吕平 , 宋晓宇 . 面向实

22、时数据的 CPS 江花 , 张思卿 . 高阶类型化软件体系统一体化建模方法系结构建模和验证及案例闭幕式 (3 楼 10会议室 )5:00pm-5:15pm主持：朱惠彪会务联系人：刘波老师（， liubocq）王勤老师（， wqi ）9第三届全国形式化方法与应用会议（FMAC 2018 ）特邀报告内容简介（一）报告题目 ： Verification of Roundtrip Property in Bidirectional Programming主讲人 ： Zhenjiang Hu(National Institute of Informat

23、ics/University of Tokyo)摘要 :Bidirectional transformations play an important role in data synchronization, data integration, and smart system construction. A bidirectional transformation consists of a pair of transformations - a forward transformation produces a target view from a source, while a put

24、 back transformation puts back modifications on the view to the source - satisfying the round trip property. However, given a pair of transformations, it is an open challenge to verify whether they form a bidirectional transformation satisfying the round trip property. In this talk, we show that und

25、er some reasonable constraints we can tackle this challenge with an automatic verification algorithm.特邀报告内容简介（二）报告题目 ： 并发 C 程序编译器验证初探主讲人 ：Xinyu Feng(Nanjing University)摘要 :编译器将源程序翻译成可执行的机器代码。若编译器中存在缺陷，人们则很难对可执行代码的正确性和安全性提供任何保证。编译器验证则通过形式化验证的方法，严格证明编译器实现的正确性。自 Xavier Leroy 团队实现对 CompCert 编译器的验证以来，编译器

26、验证成为当前形式化验证领域的一个研究热点。本报告将介绍编译器验证的主要理论基础和主要相关工作。在此基础上，我们针对 CompCert 仅支持串行 C 程序的不足，探讨如何将 CompCert 应用于无数据竞争的并发 C 程序的编译，并验证其正确性。10第三届全国形式化方法与应用会议（FMAC 2018 ）企业报告内容简介（一）报告题目 ： 形式化方法在航天的应用实践与思考主讲人 ：顾斌（航天科技集团）摘要 :航天是形式化方法的重要应用领域之一，为了提高航天器软件的可信性，工程师们一直希望把形式化方法引入到软件的研制中。本报告介绍了我们在航天器姿态和轨道控制软件研制中的一些应用实践，并探讨了一些努力的方向。企业报告内容简介（二）报告题目 ： 机会与挑战 ICT 全栈产品