一组研究人员设计了一种方法，无需传统软件测试即可验证一类复杂程序是否没有错误。该系统称为Armada，该系统利用一种称为形式验证的技术来证明某个软件是否可以输出预期的结果。它以使用并发执行运行的软件为目标，并发执行是提高性能的一种广泛方法，长期以来，将其应用到该方法中一直是一项特别具有挑战性的功能。
该合作努力密歇根大学，微软研究院和卡内基·梅隆之间的ACM编程语言设计与实现(PDLI2020)有杰出论文奖被认可。
并发程序以其复杂性而闻名，但是在处理器的原始速度开始趋于平稳之后，并发程序已成为提高性能的重要工具。通过各种不同的方法，该技术可以归结为在程序中同时运行多个指令。一个常见的示例是一次使用多个CPU内核。
另一方面，形式验证是一种证明程序将始终输出正确值而不必用所有可能的输入进行测试的方法。通过将程序作为数学证明，程序员可以证明错误或错误是不可能的，并且其执行是密封的。即使没有并发，这也克服了所有程序的共同缺点，即彻底测试某些东西可能不切实际或实际上是不可能的。
该论文的合著者ManosKapritsos教授说：“从根本上讲，除非您尝试所有可能的输入方式，否则您可能会错过一些东西。”“而且在实践中，人们确实会错过事情。我们正在谈论的系统非常复杂，无法完全尝试该系统的所有行为。”
正式验证可以代替这种详尽测试的需求。但是事实证明，生成令人满意的证明的过程非常困难且耗时，特别是当您深入研究具有并发复杂性的程序时。
“并发程序的主要挑战在于需要将许多不同的代码线程协调在一起，”在UM本科期间从事该项目工作的合著者UpamanyuSharma说。“为了验证多线程程序是正确的，我们必须对多个方法同时运行时可能发生的大量交错进行推理。”
如此大量的分支可能性很难通过逻辑公式来概念化和表达。
迄今为止，已经设计了多种证明方法来处理不同类型的并发。在这个项目中，研究人员着手设计一个单一的框架，该框架允许用户应用其中的许多技术来验证一个程序，其最终目标是尽可能减少前期的工作量。
Armada的工作方式是将经过并发设计的系统进行一系列转换，直到将其分解为更简单的表示形式。开发人员只需证明每个简化的步骤确实代表了上一步中较复杂的程序。为此，开发人员使用Armada的高级语法来描述较简单的程序，并指出支持转换所需的证明方法之一。
Kapritsos解释说：“在每次转换之后，您都需要推理出系统保持其正确性或等同于先前的正确性。”
然后，舰队的每个步骤都会自动生成证明，并通过证明者进行验证。如果证明失败，用户将更改其描述或证明方法并生成新的描述或证明方法。
