贸易公司网站源码,天元建设集团有限公司天眼查,选择常州网站建设公司,网站及其建设的心得2023年CCF中国软件大会#xff08;CCF ChinaSoft 2023#xff09;由CCF主办#xff0c;CCF系统软件专委会、形式化方法专委会、软件工程专委会以及复旦大学联合承办#xff0c;将于2023年12月1-3日在上海国际会议中心举行。 本次大会主题是“智能化软件创新推动数字经济与社… 2023年CCF中国软件大会CCF ChinaSoft 2023由CCF主办CCF系统软件专委会、形式化方法专委会、软件工程专委会以及复旦大学联合承办将于2023年12月1-3日在上海国际会议中心举行。 本次大会主题是“智能化软件创新推动数字经济与社会发展”学术、工业、教育、竞赛等分论坛活动40余场期待您的参与 目前大会火热报名中早鸟注册early-bird registration10月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、HPCAASPLOSISCASPDAC等多个体系结构和安全领域顶级会议及期刊国内外已授权专利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 ModelSCM提出了硬件结构化根因模型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取得了显著的性能提升。
