这是一套按微信公众号官方合集 “高校教学系列-程序分析” 完整整理、技术校正并重组的中文学习资料。它不是文章摘抄，而是把理论文章、实验视频、官方 YASA 文档和固定源码证据合并成可学习、可练习、可复核的体系。
截至 2026-08-28 04:06 UTC：
- 官方合集列出的文章：8/8 已归档；
- 正文内容图片：109/109 已下载并核验清单；
- 官方课程表列出 4 次理论课 + 3 次已发布实验课；再与微信合集中的 1 篇开课公告合并，形成
7+1的完整对应； - 三次实验视频：3/3 已取证，共 6,403 秒、2,155 个 ASR 时间段；
- 关键视频场景：92 帧（43/30/19），用于校正 ASR 中的技术名词和代码；
- YASA 官方公开文档：21 篇，并以本地固定的 YASA-Engine 提交交叉核验。
合集仍标记 isupdating=1，所以这里的“完整”指该时间点官方已发布的 8 篇。课程最初规划的第四次 Web 框架适配实验尚未作为独立课程发布；第三次实验确实使用 Mux 框架适配作为 Checker 编写案例，二者不能混为一谈。
完整性证据、官方链接和顺序解释见：系列索引与完整性。
| 顺序 | 资料 | 学习目标 |
|---|---|---|
| 0 | 系列索引与完整性 | 先确认范围、课程顺序和证据边界 |
| 1 | 静态分析基础与中间表示 | 不可判定性、近似、soundness、CST/AST/CFG/3AC/SSA/LLVM/UAST |
| 2 | 数据流分析 | GEN/KILL、AE/RD/Live、Worklist、Call Graph、ICFG、上下文敏感 |
| 3 | 指针分析与抽象解释 | points-to/alias、Andersen、格、区间、不动点、widening/narrowing |
| 4 | YASA 三次实验 | AST/调用图/污点、UAST/Engine、Checker 实现与复现实验 |
| 5 | 公式与术语速查 | 集中复习公式、算法与术语 |
| 6 | 练习与参考答案 | 手算、解释题、YASA 设计题和综合项目 |
建议直接采用 六周学习路线，每周都有学习内容、动手输出和掌握标准。
不可判定性与 Rice 定理
↓ 为什么必须近似
过近似 / 欠近似 / may / must / soundness 契约
↓ 在什么表示上计算
CST → AST/UAST → CFG → 3AC → SSA/LLVM IR
↓ 图上的不动点
AE / RD / Live → Worklist → Call Graph / ICFG
↓ 间接内存与过程调用
Points-to / Alias → Andersen 包含约束
↓ 统一数学框架
偏序 / 格 / 抽象域 → 不动点 → Widening / Narrowing
↓ 工程落地
YASA-UAST → Analyzer → Symbolic State → Checkpoint / Checker → Finding / Output
| 官方篇目 | 本资料位置 |
|---|---|
| 开课公告 | 00-系列索引与完整性.md、主笔记 1 的课程定位 |
| 基础概念 | 主笔记 1：不可判定性、近似、soundness/completeness |
| 中间表示 | 主笔记 1：CST/AST/CFG/3AC/SSA/LLVM/UAST |
| 数据流分析 | 主笔记 2：局部和过程间数据流 |
| 指针分析及抽象解释 | 主笔记 3：Andersen、抽象域和循环不动点 |
| YASA 原理简介及功能演示 | 主笔记 4：第一讲 |
| YASA 内部机制深入解析 | 主笔记 4：第二讲 |
| 掌握 Checker 编写艺术 | 主笔记 4：第三讲 |
微信合集的当前展示位置是 1→2→3→4→5→6→7→8，但课程学习顺序是 1→2→3→4→5→7→6→8；即实验“原理简介”先于“内部机制”。
- 勘误与概念辨析：集中列出最危险的术语混淆和文章技术问题；
- 参考资料：系列引用、YASA 官方入口、文档和固定源码链接；
- 来源与复现说明：精简后的 Markdown 资料布局、抓取命令和完整性边界；
- 微信原文可读归档：8 篇 GitHub 可读 Markdown 与正文必需的 109 张本地图；
.work/transcripts/：三次视频带时间戳 ASR，仅作检索线索；.work/lesson-scenes/：视频场景帧和 contact sheet；sources/yasa-docs/：21 篇官方公开 YASA 文档的 Markdown 快照，来源信息保留在 front matter；.work/YASA-Engine/：源码核验快照。
YASA 章节尤其强调版本和来源：
【课】：微信文章、课程视频/画面明确给出的内容；【仓】：当前官方文档、固定源码或官方项目论文可核验；【推】：为了教学而做的解释或重建，不冒充课程原话；【缺】：公开材料确实不足，例如完整 UQL 规范、受登录保护的 PDF 正文、精确课程 commit。
ASR 会把 UAST、Call Graph、CheckerPack、Source/Sink 等词识别错，因此笔记只把转写当作时间索引，并用画面、官方文档和源码校正。
- 每章先读“目标/主线”，再手算例子；
- 对照
公式与术语速查.md复述集合包含关系和方程； - 独立完成练习后再展开
<details>中的答案； - YASA 实验记录目标版本、命令、规则和输出，不把当前 API 倒灌成 2025 年课程原话；
- 遇到结论时明确：查询正例、近似方向、合并维度、终止策略和证据等级。
重新抓取官方合集：
python scripts/fetch_series.py检查 Git 中保留的资料和 Markdown 链接；若本地仍有被忽略的视频证据，再追加严格检查：
python scripts/verify_materials.py
python scripts/verify_materials.py --require-work-evidence视频、转写、场景和 YASA 文档的复现命令见 来源与复现说明。重新抓取可能改变快照；更新时必须比较 album_id、文章数量/msgid、continue_flag 和 isupdating，而不是只看网页标题。
- 本资料以释义、重算、重构和勘误为主，不替代公众号原文和视频；
- 当前 YASA 文档/源码可能晚于课程现场版本，具体 API 以目标提交为准；
- 第四次独立实验尚无官方发布，不会用普通 Mux/Django 文档伪造课程内容；
- 静态分析结论始终依赖语言语义、外部模型和 soundness 契约，不能脱离前提使用。