整数缺陷是一类与整数的有限表示相关的程序缺陷,对软件系统的可靠性和安全性均有重要影响。人工审查难以发现涉及复杂程序逻辑的、由边界输入触发的缺陷。此外,由于C的整数语义的复杂性,整数缺陷的修复是极易出错的。为了实现准确且高效的自动化整数缺陷检测与修复,本文从逻辑推理、静态分析和修复实施3个自底向上的层次开展了研究,主要内容包括:1.提出了面向多核CPU的理论域上可满足性判定的并行化框架LDC,并给出了LDC的可靠性和完备性证明。本文将该框架应用于无量词等值理论域,证明了终止性,并实现了并行SMT求解器PZ3。在SMT-LIB测试集以及随机问题上的实验结果表明PZ3能够成功加速多种不同类型问题的求解,并且其并行加速的效果胜过了最先进的基于配置组合方法的并行求解器。2.为了高效地对程序的局部性质进行精确分析,提出了基于分而治之思想的组合静态分析框架C~2PA并证明了其可靠性。本文面向C~2PA设计了一种新的C程序整数数值语义分析算法,并实现了静态分析工具Tsmart-BD。实验结果表明,Tsmart-BD在标准测试集上漏报率为0.0%,误报率为12.7%,领先于知名开源静态分析工具和软件验证工具。此外Tsmart-BD能够在7.5分钟内完整分析规模超过320kLOC的开源软件Vim。3.提出了两种整数缺陷自动修复方法:(1)对C程序的整数操作进行精度提升,以消除编译得到的可执行程序中的整数缺陷,(2)面向缺陷的基于典型修复模式的修复生成。两种方法分别实现为工具CIntFix和IntPTI,且均能正确修复测试集上的所有目标缺陷。在开源项目上,CIntFix以1.18kLOC/s的速率完成对556.416kLOC代码的变形;IntPTI能够避免对96.3%的关键程序位置的更改,且修复引入的额外时间开销仅为0.5%。本文的研究成果均已集成到软件可信保障工具集Tsmart,并在实际的列车控制系统嵌入式软件的开发流程中进行了工程化应用实践,成功发现并修复了67个新的整数缺陷。