出品人：詹乃军
中科院软件所研究员
中科院特聘研究员
中国科学院大学岗位教授

                                                                               

程序智能构造与验证

近年，随着人工智能技术的快速发展，将人工智能技术与传统程序理论结合已经成为一个趋势，特别是基于人工智能技术的程序合成，以及将人工智能技术应用于程序验证，解决传统程序验证效率和规模等挑战。
算法合成——自动应用算法模式合成高效程序
熊英飞
北京大学副教授
于2009年从日本东京大学获得博士学位，2009-2011年在加拿大滑铁卢大学工作，2012年加入北京大学，现任新体制长聘副教授。熊英飞的研究兴趣是程序设计语言和软件工程，特别是程序合成、修复和分析。他提出了理论和方法降低程序编写和缺陷修复的代价。比如，基于差别的双向变换框架是最广泛使用的双向变换框架之一，概率和逻辑结合的程序合成框架玲珑框架将程序修复的正确率从此前不到40%提升到80%以上。他的工作也被工业界采用，比如新一代Linux内核配置项目、燕云DaaS系统、华为公司等。他获得CCF-IEEE CS青年科学家奖、MODELS十年最有影响力论文奖，5次获得ACM SIGSOFT/IEEE TCSE杰出论文奖。他是SATE18的程序委员会联合主席，也在PLDI、ICSE、FSE等会议担任PC。          
内容简介：
优化程序的基本手段是应用人们总结出来的各种算法模式，但直接应用算法模式会有较大挑战。应用算法模式虽然可以看做是程序合成问题，但传统程序合成方法主要关注功能正确性，较少对合成程序进行算法优化。北京大学团队近期针对这个问题开展研究，发现很多算法模式应用的核心是一个特定的程序合成问题，称为提升问题，并针对提升问题提出了新型程序合成算法AutoLifter。本报告将介绍基于算法模式的程序合成问题，并介绍提升问题和AutoLifter算法。                                                                                                                              

演讲提纲：
1. 介绍算法合成问题和其意义
2. 介绍大模型在该问题上的应用效果
3. 介绍北京大学在该问题上的初步方法
4. 介绍初步方法的效果
5. 总结和未来展望        

听众受益：
1. 了解算法合成问题的研究意义
2. 了解一类算法问题的自动合成方法

基于机器学习的自动化AI芯片编译技术
内容简介：
AI 芯片在朝着紧耦合异构的方向不断演进，面对越来越复杂的异构芯片，性能优化是业界一直在尝试解决的关键问题。近几年学术界和产业界在基于机器学习的优化策略自动生成等方面做了大量的探索，并取得了很好的成果。本次分享将主要针对 AI 编译优化介绍地平线的一些实践，探索基于强化学习的自动化编译技术。                                                                                                                                        

演讲提纲：
1. AI芯片编译的背景和问题
2. 监督学习在AI芯片编译中的应用
3. 基于强化学习的自动化编译技术
4. 从规则驱动到数据驱动：AI时代的软硬件协同设计

听众受益：
了解机器学习在AI芯片中的应用，以及自动化编译技术的最新实践经验。                                                                
李建军
地平线编译器研发部负责人
2012年博士毕业于中国科学院计算技术研究所，2012年至2016年在计算所任副研究员，主要研究方向为动静态程序分析、编译优化、软件安全等。2016年底加入地平线，负责AI芯片的编译器及Runtime相关的研发工作，并直接参与AI芯片的软硬件协同设计开发。在AI芯片编译优化，基于机器学习的编译优化技术等方面做了大量的研究和实践。在CGO, ICSE, ASE, TACO, TPDS等国际会议和期刊上发表论文10余篇，AI芯片、编译器相关授权专利30余项。                 
复杂安全攸关嵌入式系统的形式设计与实现
王淑灵
中国科学院软件研究所副研究员
中国科学院软件研究所副研究员，硕士生导师。2008年于北京大学数学科学学院获得博士学位，2008年至2010年于联合国大学国际软件技术研究所从事博士后工作。研究方向为形式化方法、嵌入式系统形式设计、形式验证、交互式定理证明等。在TOSEM、Computer Journal、CAV、FM、RTAS等发表论文30余篇。主持面上项目或作为项目骨干参与多个重点研发计划和重大项目。                                
内容简介：
复杂嵌入式系统广泛应用于国民经济发展和国防建设的众多重要领域，如轨道交通、航空航天等。在这些领域，系统安全是至关重要的，如果发生失效将会给生命、国家安全、社会经济等带来灾难性后果，因此也被称为安全攸关系统。复杂安全攸关系统涉及计算、控制、通信技术等行为以及复杂体系结构的紧密耦合，如何开发安全可靠的复杂嵌入式软件已经成为计算机科学、控制论和应用数学共同面临的挑战。形式化方法已公认是确保软硬件系统正确性的重要途径。本报告将介绍复杂嵌入式系统的形式设计以及在此基础上实现的工具链MARS。MARS支持基于Simulink/Stateflow和AADL的协同建模和自动仿真，支持包含系统的复杂行为和体系结构的协同设计；同时，提供以HCSP为基础的形式建模、仿真和验证框架，实现了从图形模型到HCSP形式模型的自动转换；最后，支持从已验证形式模型到SystemC、C程序的自动生成。其中MARS不同层模型之间的自动转换已严格证明一致性，从而保障系统的正确性。我们的工作已应用于国家探月“嫦娥”三号软着陆、首次火星探测任务“天问一号”等重大工程。                                                                                        

演讲提纲：
 1. 背景和问题介绍
2. 基于Simulink/Stateflow和AADL的协同设计
3. HCSP形式建模和验证
4. 已验证模型到C代码的自动生成
5. 应用

听众受益：
了解算法合了解安全攸关系统软件的形式设计方法，如何对一个系统进行行为和体系结构两方面的协同设计，并保证正确性。                                                                                        
程序功能正确性证明与AI辅助证明生成
内容简介：
基于定理证明的程序验证技术是保证程序功能正确性与安全性的重要技术手段。目前，程序验证技术已经能够用于验证操作系统内核与编译器的功能正确性，但是验证所需的人力成本较大。将AI与程序验证相结合，是能够兼顾自动代码生成与生成代码准确性的未来发展方向。在AI辅助生成证明的过程中，可以由AI系统尝试生成关键断言，由基于定理证明的程序验证系统负责检验相关证明的合法性。                                                

演讲提纲：
1. 程序验证的基本原理：交互式证明与程序逻辑
2. 程序验证的现有成果：系统软件验证与程序验证工具
3. AI时代的新机遇：解决旧问题有了新武器
4. AI时代的新挑战：传统技术依旧是好工具

听众受益：
了解程序验证技术与AI相关工作的最新研究成果
曹钦翔
上海交通大学副教授
本科毕业于北京大学，博士毕业于美国普林斯顿大学，2018年回国任教，现为上海交通大学约翰霍普克洛夫特计算机科学中心副教授。长期从事基于交互式定理证明的程序验证工具开发，并研究有关程序逻辑特别是分离逻辑的理论问题，是Verified Software Toolchain（VST）工具的主要开发者之一，其首次实现了从业务逻辑，到源代码开发，再到编译的全链条功能正确性验证。                                              
京ICP备2020039808号-4
返回顶部