复杂程序正确性机器辅助证明的研究

本项目的目标是研究机器辅助证明的使用对形式化方法，特别是对复杂程序的正确性证明所产生的影响。此项研究对于改进形式化方法的研究手段，全面提高软件开发的正确性具有重要意义。.为了避免空泛，我们将采用实例研究的技术路线。以复杂程序切片算法的正确性证明为例，从应用实例的角度，对由机器辅助证明系统的应用所带来的若干个一般性问题进行研究。这样所取得的结果既是对程序切片算法这一具体问题领域的贡献，也可以作为形式化方法成功应用的一个实例。.特别是，通过具体问题的解决所获得的原创性素材，对一般性问题的解决可能起到意想不到的作用。