关于暑期学校
C* (CStar) 是一种面向C语言的开发与证明一体化语言，通过在C中引入形式化规约与证明，达到代码中程序与证明的紧耦合。这种技术不仅能在开发过程中实时验证正确性、提升软件可信度，还能通过构建高安全公共代码库、证明策略代码库以及自动证明智能体，大幅降低系统软件形式化证明的门槛与成本。
本次暑期学校将由北京大学程序设计语言研究室主办，理论与实战结合，带您理解从分离逻辑、验证条件生成到证明智能体的完整技术体系。适合对系统软件验证、形式化方法、程序语言理论感兴趣的研究者、工程师与学生。
课程资料：
http://cstarlang.org
C* 全栈实战
从概览到工具链、证明策略，手把手掌握C*开发环境与证明技术。
一体化验证
分离逻辑、前向/后向证明、验证条件生成，实时验证代码正确性。
证明智能体前瞻
自动证明策略、PSI范式与智能体，探索下一代低门槛验证方案。
课程安排 · 每日三讲
每天下午 14:00 - 17:00（每节50分钟，课间休息10分钟）
| 日期 | 第一节课 (50min) | 第二节课 (50min) | 第三节课 (50min) |
|---|---|---|---|
| 7.20 周一 | C* 概览 理念与蓝图 | C* 工具链 编辑器、验证器集成 | 逻辑基础 一阶逻辑、霍尔逻辑 |
| 7.21 周二 | 分离逻辑 堆操作推理 | 程序验证规约 前置/后置条件 & 不变式 | 验证条件生成 前向符号执行 |
| 7.22 周三 | 前向型证明 用C语言写证明 | 后向型证明（I）基本思想与Tactic | 后向型证明（II）分离逻辑证明 |
| 7.23 周四 | 操作式证明（I）基本思想与模式 | 操作式证明（II）开发与证明一体化 | PSI范式 证明(P)-规约(S)-实现(I) |
| 7.24 周五 | 证明自动化 分离逻辑命题纯化 | 证明智能体 AI辅助自动证明 | Panel：AI时代的编程语言设计 |
每日课程包含理论讲解与现场Demo，实践环节穿插证明工具操作。
教师团队
北京大学程序设计语言研究室核心师资，亲自授课指导
胡振江
教授 · 计算机学院院长
程序设计语言、程序演算、形式化方法领域著名学者，长期推动程序语言理论与系统软件验证的深度融合。
王迪
助理教授
C*研发负责人，专注开发与证明一体化、分离逻辑与验证条件生成，推动低门槛C程序验证生态建设。
熊英飞
长聘副教授
研究兴趣包括程序综合、程序修复、类型系统与验证，在软件工程与形式化方法交叉方向成果丰硕。
张昕
助理教授
研究方向包括类型系统、程序语义与形式验证，在程序逻辑与证明辅助工具方面有丰富经验，助力C*语言安全推理基础。
四位老师将共同讲授理论、工具链与证明策略，并参与实践指导
📍 北京大学
燕园校区 (具体教室开课前邮件通知)，
与顶尖学者深度交流。
面向人群
学生/科研人员/业界系统开发者，具备C语言基础及初步逻辑思维即可。
实践亮点
基于C*工具链编写带证明的代码，体验验证条件自动生成与证明策略调试。
北京大学程序设计语言研究室
北京大学程序设计语言研究室 长期深耕函数式程序设计语言、双向变换、程序演算、领域特定语言、程序分析、程序综合、程序修复、神经网络分析、形式验证与安全等领域。C* 项目致力于打造低门槛、高效率的C程序验证生态。暑期学校将开放部分研究资源，让学员体验学术界最前沿的"证明即代码"工作流。
