2023年CCF中国软件大会（CCF ChinaSoft 2023）由CCF主办，CCF系统软件专委会、形式化方法专委会、软件工程专委会以及复旦大学联合承办，将于2023年12月1-3日在上海国际会议中心举行。

本次大会主题是“智能化软件创新推动数字经济与社会发展”，学术、工业、教育、竞赛等分论坛活动40余场，期待您的参与！

目前大会火热报名中！早鸟注册（early-bird registration）10月22日截止，提前注册付费锁定注册费优惠权益。

CCF ChinaSoft 2023官方首页：

http://chinasoft.ccf.org.cn/

点击文末“阅读原文”或扫描下方二维码进入官方注册通道:

https://conf.ccf.org.cn/chinasoft2023

✦  +

+

论坛巡礼

论坛名称：形式验证@EDA论坛

时间：2023年12月01日08:30-12:30

地点：上海国际会议中心，3E会议室

论坛简介：

“形式验证@EDA”论坛聚焦于EDA中的形式验证技术，包括SAT/SMT求解、硬件模型检测、等价性验证、基于断言的形式验证、指令集一致性形式验证、信息安全性质形式验证、缓存一致性协议形式验证、乘除法器和浮点计算单元形式验证、指令集语义形式建模、硬件设计形式验证案例研究等。

EDA软件对于芯片设计开发至关重要，属于中国急需突破的卡脖子技术。形式验证是保证计算机软硬件系统正确性与安全性的非常重要的手段，已经成为EDA软件芯片设计验证工具不可或缺的组成部分，全世界三大EDA软件厂商Cadence、Synopsis、Siemens的EDA软件均包含成熟的芯片设计形式验证工具。

EDA中的形式验证技术属于跨学科研究，涉及体系结构、EDA、形式化方法、编程语言等领域，需要不同学科的专家学者分工合作才能推动该方向的快速健康发展。本论坛拟邀请中国计算机学会三个专委，即体系结构专委、集成电路设计专委、形式化方法专委，中EDA中的形式验证技术方面的专家学者一起进行交流研讨。这三个专委中均有从事该方向研究的专家学者，但三个专委之间交流较少，缺乏一个交流合作的平台。

本论坛有望成为三个专委的专家学者长期合作交流的平台，推动EDA中的形式验证技术在中国的发展，促进相关研究社区的形成，为缓解EDA卡脖子问题贡献力量。

日程安排

Schedule

论坛主席

  Forum Chair

蔡少伟（中国科学院软件研究所）

研究约束求解和EDA形式化验证。中国科学院优秀导师，《EDA技术白皮书》形式化工具领域主编，获国家优秀青年基金资助。解决了命题逻辑推理方向十大挑战的第7个挑战；设计了首个支持整数算术理论的SMT随机搜索算法。发表50多篇CCF A类论文，获得SAT 2021最佳论文奖、AIJ期刊近五年最受欢迎论文。在SAT比赛，SMT比赛，MaxSAT比赛多次获得冠军，刷新了整数规划榜单MIPLIB多个难解实例的求解记录。受邀在组合搜索算法和EDA领域的著名会议SOCS和FMCAD上做特邀报告。

侯锐（中国科学院信息工程研究所）

主要研究方向是计算机体系结构、处理器芯片设计与安全，长期从事国产自主安全可控高性能处理器芯片的研制和开发。获得国家杰出青年科学基金、优秀青年科学基金资助。在国内外期刊及会议上发表论文50余篇，包括ACM TOCS、TC、HPCA，ASPLOS，ISCA，S&P，DAC等多个体系结构和安全领域顶级会议及期刊，国内外已授权专利50余项。中国通信学会区块链专委会副主任，中国计算机学会体系结构专委会委员。

李华伟（中国科学院计算技术研究所）

长期从事处理器芯片设计和EDA相关研发工作，作为负责人承担863、973、基金重点、重点研发等国家级项目10项，获国家技术发明二等奖、北京市科学技术一等奖、中国计算机学会(CCF)技术发明一等奖等。在微处理器可靠设计方面创新了星载微处理器验证-测试-恢复技术体系，解决了抗辐照测试难题；在专用处理器自动设计方面的创新在国际上产生重要影响，获IEEE Trans. on Computers期刊2021年最佳论文奖、第37届IEEE国际计算机设计大会(ICCD’19)最佳论文奖。

吴志林（中国科学院软件研究所）

中国科学院软件研究所计算机科学国家重点实验室研究员，博士生导师， 2020年“CCF-IEEE CS”青年科学家奖获得者。长期从事计算逻辑、自动机理论、程序验证相关的研究，在知名国际会议和期刊上发表论文40余篇，包括LICS、POPL、CAV、Information and Computation、IJCAR、CADE、CONCUR等。先后主持多项国家级项目，包括国家重点研发计划课题、中科院先导项目课题、“十三五”全军共用信息系统装备预先研究项目、国家自然科学基金面上基金等。中国计算机学会形式化方法专业委员会副秘书长，国际会议ATVA 2022程序委员会共同主席，CAV、CONCUR、ATVA等国际会议的程序委员会委员。

论坛嘉宾

Forum Guests

金意儿（华为技术有限公司）

华为可信计算首席科学家，佛罗里达大学名誉教授，IEEE硬件安全与可信专委会联席主席。他的研究领域主要涉及软硬件协同安全和新兴集成电路安全，包括硬件支持的系统安全，集成电路产业链安全，以及可信自动化等。他撰写了集成电路安全一书，同时在国际知名期刊和杂志上发表了超过200篇论文，是亚洲硬件安全年会的联合创办人。他目前是IEEE设计自动化委员会的杰出讲师。他的论文获得了多项最佳论文奖，他本人也获得包括美国能源部和美国海军在内的多项杰出青年教授奖。

报告题目

“电路显微镜”-利用形式化方法查找硬件电路漏洞

摘要

在诸如片上系统、小芯片等新技术的加持下，集成电路变得日益复杂，叠加上更加复杂的软件系统，使得测试和验证整个基于芯片的软硬件系统变得非常具有挑战性。而传统的形式化方法往往只关注硬件，或者只关注软件，这就忽略了一个基本事实，即很多漏洞是软件利用了硬件的缺陷，很难明确区分是软件漏洞还是硬件漏洞。基于这一挑战，我们提出了“电路显微镜”的理念，设计了一套基于形式化方法的验证框架，用于分析特定的硬件漏洞如何通过软件触发，进而查找漏洞的硬件根源。“电路显微镜”利用了结构化根因模型（Structural Causal Model，SCM），提出了硬件结构化根因模型（HW-SCM），这一模型定义了硬件安全属性，利用增量式SMT求解器查找可能被软件利用的硬件漏洞，同时生成相应的测试向量（或测试程序），帮助提升集成电路的安全性，消除可能的安全风险。

袁军（奥卡思/阿卡思微电科技）

清华大学本科，博士毕业于德州大学奥斯丁分校。多年从事芯片形式验证及仿真验证的研发和应用，奥卡思/阿卡思微电科技创始人。撰写学术专著一部，发表学术论文多篇，获批若干专利。

报告题目

工业级形式验证工具研发的体会

摘要

过去30年，形式验证从理论到科研再走向实践，并在芯片设计行业部署过程中打磨与提升，最终成为数字芯片设计验证中不可或缺的一个重要工具和方法学。报告将介绍作者在参与这一历史进程中的观察与体验。

李暾（国防科技大学）

国防科技大学计算机学院，教授，博士生导师。主要从事电子设计自动化、微处理器设计方法、集成电路设计验证等研究。发表学术论文60余篇，获军队科技进步二等奖2项。

报告题目

微处理器敏捷设计方法中的验证问题初探

摘要

近年来微处理器设计敏捷设计方法的发展，在提升设计生产率的同时，也带来了一些新的验证问题，比如产品族的验证、面向HDSL的基于断言的验证支持、覆盖率驱动的动态验证方法调整等问题，本报告将介绍我们在这些问题上最近的一系列工作。

胡伟（西北工业大学）

西北工业大学长聘教授，博导，入选国青人才，研究方向包括集成电路硬件安全、密码侧信道分析等。在领域知名期刊和会议上发表论文80余篇，出版网络空间安全专业“十三五”规划教材1部、专著1部。主持预研重点项目、国家重点研发课题、自然基金面上等科研项目10余项。任IEEE TCAD客座编辑、硬件安全领域旗舰会议HOST和AsianHOST组委会委员、ICCAD分会主席、CCF高级会员等职。研究成果获省部级科技奖励2项。

报告题目

硬件安全属性自动提取与形式化验证研究

摘要

基于属性断言的验证技术在高隐蔽性安全脆弱性搜索挖掘方面具有显著优势。然而，安全验证和脆弱性挖掘结果的有效性严重依赖于属性质量。相关领域面临的一项关键问题在于安全属性主要依靠验证者手动书写，属性集的质量和完备性难以保证，严重制约了验证效率。报告主要介绍我们在硬件安全属性自动提取与形式化验证方面的研究进展。主要探讨如何有限仿真轨迹中自动提取与翻转率、覆盖率、信息流、故障效应相关的属性断言，并通过断言验证来实现恶意逻辑和风险路径的检测，以及故障攻击的形式化分析。

贺飞（清华大学）

清华大学长聘副教授，博士生导师。主要从事程序验证、模型检验和自动推理的研究。开发了模型检验和程序验证工具，并在中航、中车、华为等公司进行应用。在形式化方法、程序语言和软件工程的重要国际会议和期刊上发表论文80余篇。入选国家某青年人才计划和“中创软件人才奖”，曾获并行编程旗舰会议PPoPP 2022最佳论文奖、软件工程顶会ASE 2018杰出论文奖、形式化方法会议SETTA 2022最佳论文奖等。

报告题目

基于数据通路传播的硬件模型检验

摘要

模型检验能为硬件代码提供高级别的正确性保障。模型检验面临的主要挑战是状态空间爆炸。抽象是应对状态空间爆炸的有效技术。我们设计了一种数据通路传播方法，将数据通路语义通过一个规则系统应用到一种基于抽象的硬件模型检验方法中。我们实现了上述方法，并通过硬件模型检测大赛案例进行了实验，实验结果表明该方法相比于著名硬件模型检验工具AVR取得了显著的性能提升。