▲部分与会专家合影▲

2024年8月9日，第十八期CCF秀湖会议在苏州CCF业务总部&学术交流中心正式拉开帷幕，会议为期四天，就“面向大型基础软件的形式化验证技术”进行深入交流和探讨。CCF会士、中国科学院院士、上海华科智谷人工智能研究院院长何积丰，CCF会士、中国科学院院士、中国科学院软件研究所研究员林惠民等20余位专家出席会议。秀湖会议AC副主席、苏州大学教授朱巧明在开幕式上致辞。本次会议的执行主席北京大学胡振江教授、北京大学詹乃军教授、上海交通大学陈海波教授主持了会议。

▼朱巧明教授致辞▼

随着数字化和智能化设备的广泛普及，操作系统、编译器、虚拟机和数据库管理系统等大规模基础系统软件的安全性问题日益凸显，保证基础系统软件安全性是国家的重大战略需求。形式化验证是保证系统软件最高安全等级的唯一技术，通过在对代码进行严格的数学证明，保证其行为符合预期，从而消除软件安全漏洞。然而，大型基础软件的形式化验证面临着巨大的挑战。现存的形式化验证方法尽管可以达到高可信、高安全，例如seL4微内核和C编译器的形式化验证，但其开发成本巨大，难以维护。本次秀湖会议旨在汇聚程序设计语言，形式化方法，系统软件开发，系统安全方面的顶级专家共同探讨支撑高安全等级大型基础软件的形式化验证的关键技术和工具开发，明确大型基础软件形式化验证的挑战，找出一条适合于我国发展的有效途径。

▼现场 –何积丰院士作特邀报告▼

秀湖会议是CCF启动的深度研讨会品牌项目，借鉴德国Dagstuhl研讨会、日本湘南会议模式，打造小型精品学术讨论会。每期研讨会均针对某一具体前沿问题讨论交流，仅限发起人邀请的一线专家参与，不对外开放，会期3天以上，要求代表全程参会，暂隔喧嚣冗务，从容深入研讨学术问题，引导科学家、企业技术专家及教育专家们在浮躁的社会中沉下心来钻研学术。 

▼现场 –胡振江教授主持▼

CCF鼓励有新想法的会员聚集一处，自由研讨，深入讨论前沿和跨领域问题的新观点，努力营造一个为学者提供交流，启迪智慧的平台。CCF将把有建设性的新思路和新观点汇集成册，作为白皮书发表，也将提供给有关政府部门作为科技立项的参考。本次会议将产出详细报告，请关注CCF的后续报道。

秀湖会议年度合作单位腾讯、华为及金牌合作单位OPPO、联想研究院对本期会议给予了大力支持。

CCF欢迎更多会员和业界专家关注和申请秀湖会议。