随着计算机软件在社会各行各业的广泛应用,程序安全成为人们越来越关注的问题。尤其是当大量计算机软件被用于航空航天、武器、大型设备等重要领域时,对软件的安全性能和稳定性能的要求就格外的高。如何能更自动化的,准确的找出各类软件中可能存在的隐藏错误,保证程序安全,成为了一项重要的工作。而作为程序验证的关键性方法之一,模型检测是一种较为成熟稳定的技术。模型检测的关键在于对程序的建模以及对程序性质特点的形式化,在数学推演的基础上用形式化验证的方式自动的验证该程序是否符合预期的特性。计数证明是数学推理证明领域中的一种基本方法。将这种方法应用在形式化验证中,能有效地对具有无限控制系统的程序进行推理,例如理论上包含无限数量线程的程序或是包含递归过程的并发程序。然而,计数证明当前大多数情况都被用作为非正式的、手写的场合。我们希望程序验证工具能够简便的、自动化的处理问题,但是计数证明算法缺乏一种完全自动化的构造方法。本文主要围绕计数证明的自动化构造问题,以及计数证明这一方法在形式化验证中的实际使用问题做出了以下研究:首先我们通过简单的实例引入了计数证明算法的可能应用场景,并且简要介绍了构造思路与控制流网络结构的存在。接下来我们在介绍了一些基础的符号之后,正式的定义了计数证明算法,并将构造的全部过程分解为了决策流程、搜索流程、提炼流程三个部分,并对每一个流程中出现的问题都做了详细的证明。之后我们引入了与计数证明算法息息相关的控制流网络结构,并对其进行了正式的定义。最后我们通过详细举例介绍了计数证明算法与控制流网络的强大功能与特性,并且分析了在不同使用环境中可能出现的细节问题。在结尾部分,我们利用现有工具实现了计数证明算法,并分析了实验数据,给出了算法的优劣分析。