第十八期CCF秀湖会议在CCF业务总部&学术交流中心成功举办，来自学术界与工业界的二十余位专家围绕“面向大型基础软件的形式化验证技术”这一主题开展探讨和交流。本次会议的报告和讨论从大型基础软件形式化验证的理论与工具开发，操作系统形式化验证的实践及其挑战，大型基础软件形式化验证的实践与人才培养，形式化验证与AI、测试、仿真等技术的集成四个方面展开，同时就大型基础软件形式化验证与开发生态发展形成共识。
2024年8月9日至12日，第十八期CCF秀湖会议在苏州CCF业务总部&学术交流中心举办，会议为期四天，就“面向大型基础软件的形式化验证技术”进行深入交流和研讨。本次秀湖会议的执行主席为北京大学胡振江教授、詹乃军教授和上海交通大学陈海波教授。CCF会士、中国科学院院士、上海华科智谷人工智能研究院院长何积丰，中国科学院院士、CCF会士、中国科学院软件研究所研究员林惠民，南京大学卜磊教授、北京大学曹永知教授、华为诺亚方舟AI理论实验室主任李震国、华为费马实验室主任秦胜潮等20余位专家出席会议（名单后附）。秀湖会议AC副主席、苏州大学朱巧明教授出席并致辞。
-01-
特邀报告 | 开宗明义
▲朱巧明教授致辞▲
中国科学院院士、上海华科智谷人工智能研究院院长何积丰以“Unifying Theories of Bayesian Network”为题带来了本次会议的第一个特邀报告。随着非确定性在软件中的普遍使用，如何与时俱进的考察非确定性在形式化语义描述层面带来的挑战是一个重要的研究问题。何积丰院士首先介绍了连接不同形式化语义描述方法（代数语义，操作语义，指称语义）的Unifying Theories of Programming框架，随后探讨了该框架在贝叶斯网络上的新发展。近年来概率编程语言得到广泛研究，该框架具有连接贝叶斯网络和概率程序语言语义的潜力，帮助更深刻地理解概率和非确定场景下软件的理论基础。
▲何积丰院士作特邀报告▲
次日，中国科学院院士、中国科学院软件研究所研究员林惠民带来了题为“大型基础软件的形式化验证：问题与挑战”的特邀报告。林惠民院士从形式化证明的历史娓娓道来，介绍了程序形式化验证的关键进展，并强调了规约在讨论程序正确性时不可忽视。最后，林惠民院士强调了形式化验证安全攸关大型基础软件的不可替代性，并带领大家探讨在操作系统的形式化验证实践中面临的挑战。
▲林惠民院士作特邀报告▲
-02-
专题分享 | 精彩纷呈
本次会议设置了大型基础软件形式化验证的理论与工具开发，操作系统形式化验证的实践及其挑战，大型基础软件形式化验证的实践与人才培养，形式化验证与AI、测试、仿真等技术的集成四个板块专题。每个专题均安排了若干观点分享报告。嘉宾们从概率程序证明、交互式证明到自动化证明、软件证明与数学定理证明、面向形式化证明的编程语言、操作系统验证、大语言模型与形式化验证结合等多个方面介绍了自身的研究进展与应用实践，同时分享了自己的观点和看法。报告内容从形式化验证的实践经验到创新技术，从对现有形式化验证技术的总结展望到形式化验证与大语言模型结合的探索尝试，内容广泛、精彩纷呈。
专题一：大型基础软件形式化验证的理论与工具开发
左右滑动查看更多
（左起：陈明帅、关楠、曹永知、陈海波、王迪）
专题二：操作系统形式化验证的实践及其挑战
左右滑动查看更多
（左起：曹钦翔、赵永望、邹沫、李希萌）
专题三：大型基础软件形式化验证的实践与人才培养
左右滑动查看更多
（左起：秦胜潮、董威、汪宇霆）
专题四：形式化验证与AI、测试、仿真等技术的集成
左右滑动查看更多
（左起：李宣东、李屹、卜磊、李震国、田聪）
专题五：大型基础软件形式化验证的理论与工具开发
左右滑动查看更多
（左起：詹博华、贺飞、夏壁灿、吴志林、宋富）
专题六：大型基础软件形式化验证的实践与人才培养
左右滑动查看更多
（左起：詹乃军、王启新、王肇国、张苗苗）
-03-
赏湖健步 | 姑苏风光
-04-
思想汇聚 | 求同存异
胡振江
詹乃军
陈海波
▲本期会议执行主席▲
会议最后半天，与会嘉宾围绕“面向大型基础软件的形式化验证技术”进行了专题研讨，一方面在此前会议讨论的基础上进行总结并形成共识，另一方面就如何聚焦大型基础软件形式化验证的挑战、促进形式化验证产学研结合发展发出倡议。经过热烈的讨论，嘉宾们围绕大型基础软件形式化验证的理论、大型基础软件形式化验证的工具开发、操作系统形式化验证的实践、AI与形式化验证的集成等方面达成初步的共识。
CCF将持续推进相关话题的讨论与总结，请持续关注CCF的后续报道。
秀湖会议是CCF全新打造的小型精品国际学术讨论会品牌，借鉴德国达堡研讨会（Dagstuhl Seminars）、日本湘南会议模式，旨在深入探讨计算机相关领域的科学、技术、应用、教育和产业等问题，为未来计算技术的发展和应用提供新思路和新建议。每个研讨会均针对某一个具体的前沿问题讨论交流为主，仅限发起人邀请的一线专家参与，不对外开放，会期3天以上，要求参会者全程参会，不能中途离会，引导科学家、企业技术专家及教育专家在浮躁的社会中沉下心来钻研学术。
参会专家名单
特邀嘉宾（姓氏拼音排序）
何积丰 同济大学
林惠民 中国科学院软件研究所
参会嘉宾（姓氏拼音排序）
卜 磊 南京大学
曹钦翔 上海交通大学
曹永知 北京大学
陈明帅 浙江大学
董 威 国防科技大学计算机学院
关 楠 香港城市大学
贺 飞 清华大学
李希萌 首都师范大学
李宣东 南京大学
李 屹 华为
李震国 华为诺亚方舟实验室
秦胜潮 费马实验室（华为）
宋 富 中国科学院软件研究所
田 聪 西安电子科技大学
汪宇霆 上海交通大学
王 迪 北京大学
王启新 香港理工大学
王肇国 上海交通大学
吴志林 中国科学院软件研究所
夏壁灿 北京大学数学科学学院
詹博华 华为
张苗苗 同济大学
赵永望 浙江大学
邹 沫 华为
会议发起人
胡振江 北京大学计算机学院
詹乃军 北京大学计算机学院
陈海波 上海交通大学/华为
会议学生助手
曹奕远 北京大学
王自然 中国科学院软件研究所
秀湖会议年度合作单位腾讯、华为及金牌合作单位OPPO、联想研究院对本期会议给予了大力支持。
CCF秀湖会议主题预告：
CCF欢迎更多会员和业界专家关注和申请秀湖会议。
联系邮箱：bls@ccf.org.cn