一份写给研究生和软件分析爱好者的形式化阅读地图，帮助你跨过程序分析论文中定义与公式的门槛。

从图灵追问什么是计算，到现代工具验证真实软件：沿着关键人物与思想，重走程序语言形式化近百年的历史。

大模型生成的代码看起来正确，就真的值得信任吗？从测试、验证与证明出发，重新理解 AI 编程时代的可靠性边界。

静态分析不可能同时拥有绝对准确、极致速度和无限规模。读懂可靠性、精度与工程成本之间真正的取舍。

循环会反复产生新状态，静态分析为什么仍能停下来？从传递函数、工作列表到不动点，看懂分析器的运转方式。

无法枚举程序的每一个具体状态时，分析器如何继续工作？用符号抽象、格和合并操作抓住真正重要的信息。

代码究竟可能走到哪里？从控制流图和程序状态出发，跟着执行路径读懂操作语义中的判断与推导规则。

论文里的集合、箭头和希腊字母总让你卡住？从程序状态出发，学会把形式化定义重新读成熟悉的程序概念。

Mac 已经连上 VPN，Ubuntu 虚拟机却仍无法访问外网？本文从 VMware 网络模式到代理转发给出完整排查与配置步骤。

Bring mutable state into denotational semantics by modeling locations, stores, expressions, and commands in a typed lambda calculus with effects.