本论坛旨在探讨形式化方法在系统软件中的应用，可以激发新的研究与开发方向，推动技术革新，促进形式化方法的理论研究成果向真实系统应用转移，加速这些方法在实际系统软件开发中的应用。同时，提供一个形式化专家与系统软件专家交流的平台，使学者、工程师和行业专家能共同探索形式化方法在不同领域的应用，碰撞出火花，推动形式化和系统软件领域的共同进步。
本次论坛报告邀请到了来自高校院所和工业界的多位大咖，涵盖了形式化方法在操作系统、编译器、数据库、网络基础设施、工业软件、区块链、并发系统、视窗界面等方面的研究进展，欢迎各位专家和学者前来参加。
01
论坛组织委员会
王肇国（上海交通大学）
付明（华为）
卜磊（南京大学）
02
论坛议程
03
论坛报告嘉宾简介
孙猛
报告题目：基于mediator的区块链共识协议建模与验证
报告摘要：
近年来，随着5g、物联网、区块链等技术的飞速发展，各式各样的共识协议正在起着越来越重要的作用，它们的安全性、可靠性也需要更加严格的保障。mediator是一种基于自动机的轻量级形式化建模语言，在该语言中，组件之间的通信交互通过可组合的连接件完成，组件内部的行为则通过自动机的形式进行定义。本次报告中将介绍我们在mediator语言的基础上关于区块链共识协议建模和验证的工作。
报告人简介：
孙猛，北京大学数学科学学院信息与计算科学系教授， ccf形式化方法专委执行委员，ccf区块链专委执行委员，csiam区块链专委常务委员，csiam金融科技与算法专委常务委员，caai人工智能逻辑专委委员。主要研究领域为程序理论、软件形式化方法、信息物理系统、深度学习、区块链与智能合约，主持及作为主要成员参与国家自然科学基金、重点研发计划等国家及省部级项目十余项，在tse、icse、fse、aaai、fm等期刊及会议发表论文百余篇，获tase2015、sbmf2017等多个国际会议最佳论文奖，曾任icfem2018、tase2023、facs2024、icfem2024等多个国际会议程序委员会主席及fm、tacas等国际会议程序委员会委员。
付明
报告题目：端到端高性能安全并发的工业实践
报告摘要：
后摩尔定律时代，硬件趋向于多核异构，高可靠和高性能的多核并发是高效发挥多核算力的关键，而多核体系结构下的弱内存序、异构等硬件特性给并发带来了新的挑战。本报告将介绍应用形式化方法构建端到端高性能安全并发软件栈的一些工业实践。
报告人简介：
付明，博士毕业于中国科学技术大学，操作系统和形式化方法技术专家，华为菲尔兹实验室主任。2017年加入中软os内核实验室，带领形式化验证团队从事内核设计、开发和验证工作，2019年外派德国创建德累斯顿研究所，主要研究方向是操作系统、并发理论和并发程序形式化验证，致力于将形式化方法应用于工业系统软件的开发中，在形式化方法、程序语言理论和操作系统等领域的顶会 popl 、 cav 、 sosp 、 osdi 、 asplos 、 usenix atc 上发表多篇论文，并获得 asplos '21杰出论文奖。
卜磊
报告题目：基于运行时建模与验证的实时工业软件可信构造与保障
报告摘要：
实时工业软件系统内部行为离散、连续交织，极其复杂；而外界复杂工况与动态生产需求更近一步加剧了相关系统行为复杂度，使其可信构造与保障难以进行。针对此问题，我们提出了一种基于形式化建模与验证的实时系统可信构造与保障方法。首先我们提出了一种面向可重构系统的基于场景的层次化建模语言，来对系统动态行为进行快速建模。基于此建模语言，我们在运行时对系统短期内行为进行快速建模与验证，从而对潜在不安全行为进行发现与预警。在此基础上，我们进行运行时细粒度控制参数自动生成，在发现潜在危险时，接管系统控制，保障安全。部分成果已在列控、工控等领域进行应用验证，取得广泛关注。
报告人简介：
卜磊，教授，博士生导师，现任南京大学软件学院副院长，兼任 ccf 系统软件专委秘书长；2010年在南京大学计算机与科学技术系获取博士学位；曾在cmu、msra等科研机构进行访学与合作研究；主要研究领域涉及软件工程、可信软件、形式化方法等方面，部分创新性工作发表在相关领域重要期刊与会议如《中国科学》、tcad、tc、tdsc、cav、rtss、icse、issta、ase、dac等上；入选国家级青年人才计划、高校计算机专业优秀教师奖励计划、ccf-ieee cs青年科学家奖、中创软件人才奖、nasac青年软件创新奖、ccf青年人才发展计划、msra铸星计划等
翟恩南
报告题目：面向全球规模的云网络基础设施形式化验证体系
报告摘要：
作为全球最大的云服务提供商之一，阿里云正在为全球超过 10 亿客户提供服务。为确保全球规模的服务质量，底层的云网络基础设施可靠性和正确性至关重要。特别随着ai、深度学习等算力密集型服务的兴起，云网络基础设施的可靠性遇到了前所未有的挑战。本次报告将为大家介绍过去5年我们在阿里云建立的一系列基于形式化方法的网络可靠性创新成果：我们通过打造意图驱动的智能运维体系保障网络可靠性，涉及到全球网络配置形式化验证、水位流量验证以及可编程数据面验证等。这些工作共发表多篇国际顶级的网络系统论文，如 sigcomm 和 nsdi 等，且均在阿里云规模化部署。
报告人简介：
翟恩南，阿里云基础网络研究负责人，资深技术专家。2015 年于耶鲁大学计算机系获博士学位，随后担任耶鲁大学研究型助理教授，2018 年加入阿里巴巴。主导阿里云智能化网络可靠性运维体系，确保巴黎奥运、北京冬奥等阿里云直播网络 0 故障。研究领域包括计算机网络、分布式系统等，先后在这些方向的国际顶级会议如 sigcomm、nsdi 等累计发表 60 余篇论文（包括 sigcomm 13 篇）。多次担任 sigcomm、nsdi 等国际顶级会议程序委员会委员。现任 ccf 互联网专委常委与分布式计算专委常务委员。获 sigcomm 最近论文优胜奖、获通信学会技术发明一等奖一次。
蔡少伟
报告题目：smt技术在智慧视窗布局的应用
报告摘要：
如今的ui界面不仅局限于静态的布局设置，而是逐渐向着智能化和个性化的方向发展。自适应布局能够实时响应用户的操作，以及应用场景的变化，从而提供更为精准和效率的用户界面。这本质上是一个约束求解问题，本报告介绍基于smt技术求解ui自适应布局，通过定制smt求解器，达到手机等终端的毫秒级反应。
报告人简介：
蔡少伟，中科院软件所研究员，ccf杰出会员和杰出讲者，研究约束求解和形式化验证，获得相关领域顶级会议cav，sat，cp等会议的最佳/杰出论文奖，多次获得sat比赛和smt比赛的冠军，带领团队研发了eda形式化验证工具，并进行了产业应用。
李屹
报告题目：构建与操作系统开发深度协同的形式化工具平台
报告摘要：
形式化证明是保障软件安全可信的重要技术之一，在数学假设和模型粒度合理的情况下，通过形式化技术甚至可以严格证明软件的正确性。然而与此同时，形式化证明也因为其成本较高，需要持续的投入，而让很多开发团队对此敬而远之，抑或是浅尝辄止。根据团队多年以来的操作系统形式化证明和自动形式化证明工具开发经验，我们认为形式化技术其实完全可以通过不同的形式，与软件开发团队深入整合，从而让形式化技术成为软件开发者如臂使指的工具。在本报告中我们希望介绍本团队在形式化技术“飞入寻常百姓家”方面的努力，经验和教训，以帮助大家了解形式化验证的边界，更好的将形式化技术运用在日常开发中去；同时也希望让形式化方向的研究者理解真实工程中的场景和考量，能够探索对于工业界开发团队更有意义的形式化证明技术。
报告人简介：
李屹，北京大学数学科学学院博士，华为中央软件院os内核实验室技术专家，形式化团队负责人。主要研究领域为软件形式化证明，系统安全，模型驱动开发等。带领os内核实验室形式化证明团队共同构建了自研形式化验证平台veri-hammer，通过中间验证语言来一站式支持严格形式化证明，基于形式语义的程序分析与代码生成等多种形式化技术。基于自研形式化平台完成了鸿蒙内核的证明工作，支撑其成为业界通用操作系统内核领域首个通过cc eal 6 等级公开认证的商用os内核。
罗川
报告题目：布尔可满足性采样及其在编译器等软件测试中的应用
报告摘要：
布尔可满足性（sat）采样是计算机科学中的一个基本问题。给定一个合取范式（cnf）公式，sat采样问题的目标是生成一组满足赋值，并确保这组满足赋值具有高度多样性。相比于仅需找到一个满足赋值的sat问题，sat采样问题在理论上更具挑战性。此外，sat采样在保障关键系统软件的可靠性等方面有众多实际应用。由于sat采样问题的高度复杂性，现有的sat采样方法普遍面临严峻的可扩展性挑战，即它们无法有效地解决大规模实例。本次报告介绍了一种新颖且高效的sat采样算法。在大量实例上的实验表明，本次报告提出的sat采样算法比当前最先进的方法表现更佳。值得一提的是，本次报告提出的sat采样算法已被应用于软件测试，为基础编译器（如gcc、llvm以及华为毕昇编译器）检测到了二十余个新的缺陷。
报告人简介：
罗川，北京航空航天大学软件学院副教授，博士研究生导师。已入选中国科协青年人才托举工程、中国计算机学会（ccf）青年人才发展计划。迄今总计发表ccf-a类论文40余篇，其中报告人以第一作者或通讯作者身份发表ccf-a类论文20余篇。谷歌学术引用超过1800次。担任多个ccf-a类国际顶级会议的（资深）程序委员会成员。作为负责人主持多项科研项目，包括国家重点研发计划课题、国家自然科学基金项目、ccf-华为胡杨林基金系统软件专项等。报告人在国际知名约束求解竞赛（国际sat求解竞赛、国际maxsat评测竞赛）中共获得了17次冠军，包括获得亚洲首冠。所提出的约束求解技术被国际知名学者（包括诺贝尔奖得主等）实际使用，帮助取得了巨大的经济效益；同时，研究成果被顶尖科技企业（包括华为、微软等）应用落地，有效提升了关键系统软件的性能和可靠性。
王肇国
报告题目：sql等价性验证及应用
报告摘要：
sql等价性是数据库系统研究中的根本问题，本次报告将介绍我们对sql等价性验证的最新研究及其在sql优化过程中发挥的重要作用。具体来讲，我们将先介绍最新的sql等价性验证理论lia*-t，它能够有效解决sql等价性验证中聚合函数等特性带来的挑战。在此基础上，我们开发了新的sql等价性验证器sqlsolver，可以涵盖sql 1999标准中的绝大部分特性。然后，我们将介绍基于sqlsolver开发的sql重写优化系统wetune，受超优化思想启发，通过结合暴力枚举与形式化方法，可以根据应用需求自动合成sql优化规则，有效提升web等应用中的sql执行效率。
报告人简介：
王肇国，上海交通大学长聘副教授， 软件学院副院长，国家优秀青年科学基金获得者，重点研发计划项目负责人。主要从事数据库系统与理论研究，成果发表在osdi、sigmod、vldb、nsdi、ppopp、podc等相关领域权威会议上。获2023 acm sigmod研究亮点奖、sigmod 2022最佳论文优胜奖（honorable mention）、acm chinasys新星奖、华为奥林帕斯先锋奖，以及两次华为火花奖。学术兼职包括openharmony技术指导委员会智能数据管理tsg负责人、acm chinasys秘书长、ccf学术工作委员会委员、ccf系统软件、数据库、高性能专委执委、fcs青年编委。曾受邀担任eurosys 2025、nsdi 2024、socc 2024/2023等国际会议的程序委员会成员。
04
论坛组织委员会简介
论坛主席：王肇国
个人简介：
王肇国，上海交大长聘副教授，软件学院副院长，国家优秀青年科学基金获得者，重点研发计划项目负责人。主要从事数据库系统与理论研究，成果发表在osdi、sigmod、vldb、nsdi、ppopp、podc等相关领域权威会议上。获2023 acm sigmod研究亮点奖、sigmod 2022最佳论文优胜奖（honorable mention）、acm chinasys新星奖、华为奥林帕斯先锋奖，以及两次华为火花奖。学术兼职包括openharmony技术指导委员会智能数据管理tsg负责人、acm chinasys秘书长、ccf学术工作委员会委员、ccf系统软件、数据库、高性能专委执委、fcs青年编委。曾受邀担任eurosys 2025、nsdi 2024、socc 2024/2023等国际会议的程序委员会成员。
论坛主席：付明
个人简介：
付明，博士毕业于中国科学技术大学，操作系统和形式化方法技术专家，华为菲尔兹实验室主任。2017年加入中软os内核实验室，带领形式化验证团队从事内核设计、开发和验证工作，2019年外派德国创建德累斯顿研究所，主要研究方向是操作系统、并发理论和并发程序形式化验证，致力于将形式化方法应用于工业系统软件的开发中，在形式化方法、程序语言理论和操作系统等领域的顶会 popl 、 cav 、 sosp 、 osdi 、 asplos 、 usenix atc 上发表多篇论文，并获得 asplos '21杰出论文奖。
论坛主席：卜磊
个人简介：
卜磊，教授，博士生导师，现任南京大学软件学院副院长，兼任 ccf 系统软件专委秘书长；2010年在南京大学计算机与科学技术系获取博士学位；曾在cmu、msra等科研机构进行访学与合作研究；主要研究领域涉及软件工程、可信软件、形式化方法等方面，部分创新性工作发表在相关领域重要期刊与会议如《中国科学》、tcad、tc、tdsc、cav、rtss、icse、issta、ase、dac等上；入选国家级青年人才计划、高校计算机专业优秀教师奖励计划、ccf-ieee cs青年科学家奖、中创软件人才奖、nasac青年软件创新奖、ccf青年人才发展计划、msra铸星计划等
