ChinaSoft 论坛巡礼 | CCF-华为胡杨林基金-形式化方法专项论坛

nbsp; +

+

论坛巡礼

本文特别介绍将于11月25日举办的【CCF-华为胡杨林基金-形式化方法专项】论坛。

论坛名称：CCF-华为胡杨林基金-形式化方法专项论坛

时间：2022年11月25日14:00-18:00

论坛简介：

“CCF-华为胡杨林创新基金”是由华为与中国计算机学会联合发起，致力于为海内外高校及科研院所的学者搭建产学研合作及学术交流的平台。本次研讨会邀请了获得2022年“CCF-华为胡杨林创新基金”形式化方法专项资助的优秀学者进行项目进展介绍及技术交流，旨在进一步明确项目的方案、技术与应用场景，加强学术界与工业界合作，促进形式化方法的研究和发展。

日程安排

Schedule

秦胜潮

华为资深技术专家，形式化验证科学家。目前担任费马实验室主任，负责形式化技术研究和工程能力建设。北京大学学士（1997）和博士（2002）。博士毕业后在新加坡国立大学担任新加坡-MIT联盟计算机科学研究员。2005年起在英国Durham和Teesside大校任教，历任讲师、正教授、科研副院长等职。2021年加入华为香港研究所。

主要研究领域包括软件理论与形式化方法，软件工程，程序语言等。研究工作主要涉及形式化规范和建模，程序理论和程序逻辑，程序分析与验证等。

论坛主持人

  Forum Host

熊家文

可信测试工程实验室/费马实验室高级工程师，华东师范大学博士。

主要研究领域为形式化方法、软件工程。目前于费马实验室从事系统设计的形式化验证技术探索、工程工具落地规划、设计、实施及项目管理等工作。

论坛嘉宾

Forum Guests

符鸿飞（上海交通大学）

主攻形式验证的前沿理论，在概率系统模型检验、概率程序形式验证、循环不变式自动生成方面作出基础性理论贡献。

先后在形式化方法以及程序语言理论国际著名学术会议及期刊POPL、PLDI、OOPSLA、CAV、ICALP、TOPLAS等发表二十余篇学术成果，涵盖可判定性、计算复杂性、验证算法以及相关数学理论等形式验证的各个基础理论层面。获2013年度信息物理系统形式验证国际学术会议HSCC最佳学生论文奖。概率程序形式验证方面的部分成果发表于由剑桥大学出版社出版的专著章节中。

报告题目

基于ACSL语法以及Frama-C平台的数组指针循环不变式自动生成工具实现

摘要

循环不变式自动生成是程序验证中的经典问题，在很多关键程序性质的形式验证方面有广泛的应用。数组与指针是程序中重要的数据类型，因此针对数组以及指针的循环不变式自动生成在程序验证中占有重要的地位。在本报告中，讲者将介绍在基于ACSL语法以及Frama-C平台的数组指针循环不变式自动生成工具的实现中，所采取的循环不变式生成策略以及在一些实例上的实际效果。

王竟亦（浙江大学）

浙江大学百人计划研究员。分别于2013年和2018年从西安交通大学和新加坡科技设计大学获得本科和博士学位，新加坡国立大学Research Fellow。

主要研究兴趣是软件工程、形式化方法与系统安全、隐私等。多项研究成果发表于国际顶级会议和期刊如ICSE、S&P、TSE、FM、TACAS等。曾两次获得ICSE的杰出论文奖（ICSE 2018/2020），其中ICSE 2020人工智能公平性测试文章同时入选ACM SIGSOFT Research Highlights。

报告题目

基于NLP的安全协议自动化建模技术研究

摘要

安全协议，如加密认证协议等，被广泛用于安全的应用程序级数据传输和访问控制，如TLS、WPA2等。针对安全协议的形式化验证技术可以严谨地证明该类协议在设计层面免受特定攻击的影响或用于发现潜在的隐蔽攻击向量。然而，安全协议本身的高复杂度和当前广泛应用的协议形式化建模工具所需要的的专家知识，使得基于人工的协议形式化建模成本高昂且极易出错，为形式化验证技术在现实世界复杂安全协议上的应用带来了极大瓶颈和挑战。本报告将介绍一些借助NLP技术从协议设计文档中更高效地提取形式化模型来进行安全验证的初步尝试。

甘庭（武汉大学）

武汉大学计算机学院讲师。2017年毕业于北京大学数学科学学院，获得博士学位。CCF形式化方法专业委员会执行委员。

主要从事程序和混成系统形式化验证、自动推理、约束求解研究，在中国科学、软件学报、CAV、IJCAR、AAAI、IJCAI、KDD、IEEE TAC、JSC等国内外著名会议和期刊上发表学术论文10余篇。主持国家自然科学基金青年基金项目1项。

报告题目

基于非线性Craig插值技术的程序不变式自动生成

摘要

形式化方法是保障计算机系统可靠性与安全性的有效手段，而循环不变式自动生成则是形式化方法中最为困难和最为重要的问题之一。非线性公式在程序验证和嵌入式系统验证中经常出现，特别是安全攸关嵌入式系统的控制软件。本报告研究线性与非线性循环程序的非线性不变式生成问题，基于非线性Craig插值生成的技术和思想，提出循环程序的非线性不变式自动生成方法。

祝义（江苏师范大学）

江苏师范大学教授、硕士生导师、副院长，CCF高级会员，CCF形式化方法专委会委员，江苏省计算机学会理事。

主要从事研究方向为软件可靠性、智能化软件、自适应学习等，近年来，主持国自科面上项目1项、CCF-华为胡杨林基金项目1项、省部级项目6项。担任《TSE》《INS》《SPE》《计算机学报》等期刊审稿专家。在国内外重要期刊及会议上发表论文50余篇，其中SCI/EI检索40余篇，获国家发明专利4项，软件著作权15项。个人入选江苏省“333高层次人才培养工程”中青年科学技术带头人、“南京321计划”人才，获淮海科学技术奖等奖项。

报告题目

面向CPS时空约束的资源建模及其安全性验证方法

摘要

信息物理融合系统CPS(Cyber Physical System)是在环境感知的基础上，集合物理与计算的系统，可以实现与环境的智能交互。CPS信息物理空间的不断变化对CPS资源安全性造成一定的挑战。因此，如何研究这一类由时空变化而导致的CPS资源安全性问题成为关键。本报告针对该问题提出了面向CPS时空约束的资源建模及其安全性验证方法。首先， 在TCSP(Timed Communicating Sequential Process)的基础上扩展资源向量，提出时空资源通信顺序进程DSR-TCSP(Duration-Space Resource TCSP)，使其能够描述CPS拓扑环境下的资源;其次，从时空约束的资源安全性需求中获取时间安全需求，通过DSR-TCSP的时间属性验证算法对时间安全需求进行验证;再次，将满足时间安全需求的模型转换为偶图与偶图反应，并输入到偶图检验工具BigMC中，验证其物理拓扑安全需求，对没有通过验证的反例，修改DSR-TCSP模型，直至满足所提出的安全需求;最后，通过一个驾驶场景实例，验证该方法的有效性。

来源：pengxin_ce