程序分析探讨

孙军 现任新加坡管理大学教授，其主要研究领域涵盖形式化方法、软件工程及安全等相关方向，个人兴趣包括登山、攀岩等活动。

若希望深入获取与程序分析相关的专业技术资讯，诚邀您参与编程语言技术社区 SIG-程序分析。

参与途径：文章结尾处提供小助手的微信联系方式，添加时请注明申请加入 SIG-程序分析。

---

目录

引言

程序分析很难!

知道什么是程序正确性很难！

程序分析技术很多!

自动定理证明研究

逻辑表达方法解析

举个栗子

小结

抽象解释

如何选择适合的抽象域

举个栗子

小结

其他常见方法概述

当前程序分析研究领域浅析

总结

---

#引言#

程序分析 是以特定编程语言编写的软件为对象，对其运行机制进行剖析，并通过自动化手段评估其正确性与执行效率等特性的过程。

尽管经历了数