关于暑期学校
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 周二 | 分离逻辑 (堆操作推理) | 程序验证规约 前置/后置条件 & 不变量 | 验证条件生成 VC生成技术与实践 |
| 7.22 周三 | 前向型证明 (forward proof) | 后向型证明 (I) 基本思想与规则 | 后向型证明 (II) 进阶案例分析 |
| 7.23 周四 | 操作式证明 (operational proof) | 自动证明策略 策略组合与重写 | PSI范式 证明即程序的结构 |
| 7.24 周五 | C* 架构 语言设计与实现 | 分析验证结合 静态分析+证明协同 | 证明智能体 AI辅助自动证明展望 |
每日课程包含理论讲解与现场Demo，实践环节穿插证明工具操作。
教师团队
北京大学程序设计语言研究室核心师资，亲自授课指导
胡振江
教授 · 计算机学院院长
程序设计语言、程序演算、形式化方法领域著名学者，长期推动程序语言理论与系统软件验证的深度融合。
熊英飞
长聘副教授
研究兴趣包括程序综合、程序修复、类型系统与验证，在软件工程与形式化方法交叉方向成果丰硕。
王迪
助理教授
C*研发负责人，专注开发与证明一体化、分离逻辑与验证条件生成，推动低门槛C程序验证生态建设。
三位老师将共同讲授理论、工具链与证明策略，并参与实践指导
📍 北京大学
燕园校区 (具体教室开课前邮件通知)，
与顶尖学者深度交流。
面向人群
学生/科研人员/业界系统开发者，具备C语言基础及初步逻辑思维即可。
实践亮点
基于C*工具链编写带证明的代码，体验验证条件自动生成与证明策略调试。
北京大学程序设计语言研究室
北京大学程序设计语言研究室 长期深耕函数式程序设计语言、双向变换、程序演算、领域特定语言、程序分析、程序综合、程序修复、神经网络分析、形式验证与安全等领域。C* 项目致力于打造低门槛、高效率的C程序验证生态。暑期学校将开放部分研究资源，让学员体验学术界最前沿的"证明即代码"工作流。
