中文摘要：

本项目对自动程序修正的关键技术进行了卓有成效的探索，并将研究成果应用于更为广泛的领域。首先，针对抽象精炼算法的两个主要分支-反例导引和证明导引方法，分别研究了他们的支撑算法-反例压缩和不可满足子式求解算法，在提高算法效率方面取得了突破性的进展；其次，将不可满足子式求解算法扩展到非量化一阶逻辑，从而将程序修复的求解范围从传统的命题逻辑，扩展到包含数组、指针、算术运算和未解释函数等复杂元素的真实程序；再次，将上述研究成果应用于对偶综合领域，以高效的生成高性能通讯系统的正确电路描述。项目期间，发表论文11篇，其中EI检索6篇，项目负责人在微电子领域顶级国际会议ICCAD'09发表的论文，标志着本项目的研究成果达到了国际领先水平。同期，获得军队科技进步一等奖1项，三等奖1项，培养毕业博士生1人。本项目提出的理论框架和实现技术，能有效降低自动程序修正算法的运算复杂性、扩展其可解范围，并在对偶综合领域获得了成功应用。其研究成果能够极大的提高VLSI 系统设计与验证效率，具有重大的学术价值和应用前景。