本发明公开了一种基于抽象语法树和定理证明的局部敏感程序分析方法，包括：对程序代码构建出没有语法错误的抽象语法树AST；遍历程序代码的抽象语法树AST，收集待检测节点及待检测节点的相关节点，根据待检测节点及其相关节点信息，形成待检测节点的相关逻辑表达式，输入至定理证明器中；定理证明器通过逻辑表达式求解待检测节点，若求解获得的待检测节点值存在异常情况，则判定程序存在语义缺陷。本发明通过收集程序节点局部上下文和局部路径信息，避免某些错误的报警以及提高易用性，实现了对程序代码的语义缺陷检测，避免了传统的符号执行工具分析代码因为路径爆炸问题而耗时长的问题。