今天的软件程序的大小和复杂性使得检查它们可能的可靠性变得很困难。
测试只能到此为止:通常在应用程序发布之后，这是一种等待和观望的策略，当重大问题变得明显时，开发人员会为产品发送补丁。
瑞士联邦理工学院(Ecole Polytechnique Federale de Lausanne或EPFL)的两名计算机科学家希望改变这一现状——使用自动推理工具，用更精确的正式数学证明来取代通过测试验证软件。
虽然这些年来验证工具有了显著的发展，但一个障碍是对使用数学归纳法的证明的支持。
贫穷和盗版使罗马尼亚成为欧洲软件开发的重镇
罗马尼亚近三分之二的电脑至少运行一个非法软件，这是该国技术传统的一个标志，意味着该国现在拥有欧洲人均最多的技术工人。
由自动推理与分析实验室副教授兼博士后研究员Andrew Reynolds进行的EPFL研究通过改进可满足性模理论(SMT)求解器中的归纳推理克服了这一问题。
SMT解决方案是用于软件的下一代验证程序，增强它们执行自动数学归纳法的能力将使它们能够“解决软件和硬件验证等领域的更多问题，”Viktor Kuncak说。这将反过来使软件更可靠，提高我们每天使用的系统的安全性，从空中交通管制到健康监测器。
EPFL方法依赖于证明，如果一个定理对一个自然数成立，那么它对下面的自然数(即n+1)成立。特别是在无法直接验证某个操作的情况下，该技术会将任务分解成可以解决的小任务。
“挑战通常在于发现中间引理或子目标，这是证明成功所必需的。在软件验证的上下文中，子目标可以声明一个函数调用返回的输出的特定属性，或者声明一个属性在程序执行期间始终保持不变，”Reynolds说。
从历史上看，发现这样的子目标依赖于开发人员。现在新的研究表明，这可以通过自动推理工具来实现。
合并归纳使得求解器——无论是与商业验证工具(如Coverity)一起使用，还是与开源学术工具(如Leon)一起使用，都更加强大，构建起来也更加简单。
这项新技术已经在CVC4(协作有效性检查器)中公开可用，这是一个开源的SMT解决方案。
对于软件验证应用，该工具能够自动证明数据结构的正确性，包括二叉搜索树和排序列表。在某些情况下，该工具能够发现比用户手动检查更简单的证明，”雷诺兹说。
“我们希望数学家和计算机科学家能够专注于数学证明中最具挑战性的部分，同时允许底层的自动推理工具来处理证明中的大部分步骤。”
“通过增加用于数学证明的自动化程度，我们同样也增加了我们能够自信地推理的定理和系统的规模和复杂性。”