Expressive Multi-theory Reasoning for Interactive Verification

由一组杰出的研究人员和工业用户建立，计算机科学的大挑战#6是可靠的系统进化：GC6的愿景是未来所有的计算机系统都证明社会对它们的信任是正确的。可靠的一个关键概念是可验证性，也就是说，人们可以保证计算机系统做它应该做的事情。可验证性的最高可能级别称为形式验证，它生成系统可靠性的数学证明。硬件和软件的正式验证现在广泛用于关键任务的实际应用程序中。这些代码包括美国宇航局深空探测器中的嵌入式代码，英特尔和AMD cpu中的算术芯片，以及微软Windows等大型消费者操作系统中的设备驱动程序代码。为了达到最高水平的质量保证，正式验证现在是测试和模拟的必要补充。形式验证主要依赖于用于描述系统的数学理论的证明方法的自动化。自动证明可以演绎法完成，通过组合简单的证明规则，或非演绎法完成，通过直接利用我们对这些理论的知识。非演绎证明速度快，但演绎证明的可靠性更明显，因为它可以被分解成简单的片段。在一个理想的世界里，非演绎证明自动化程序被用作演绎证明的预言机。难点在于如何用非演绎程序的答案推导出演绎版本。实现非演绎和演绎证明自动化程序的干净和有用的集成是一个重要的问题。我们的研究关注一种相对较新但广泛部署的非演绎证明程序的证明，称为SMT求解器。这些是专门的程序，用于自动证明有关计算机系统行为的断言，当这些断言被表示为数学公式时。我们计划增强SMT求解器，以允许表达更复杂的断言，然后探索加速SMT求解器生成的答案的演绎分析的方法。这两个目标都将提高工业强度形式验证的有效性。在这项工作中，我们得到了工业界和学术界的大力支持。在之前的相关工作中，我们在布尔问题求解器的演绎分析中实现了数千倍的加速，首次使演绎验证在工业布尔问题上可行。我们对重复这一成功寄予厚望。成功将意味着大大提高演绎验证的能力，从而有能力为比目前可能的更为复杂的计算机系统提供可靠的高水平质量保证工具包。

As established by a panel of distinguished researchers and industrial users, Grand Challenge #6 for computer science is Dependable Systems Evolution: The vision of GC6 is of a future in which all computer systems justify the trust that society increasingly places in them. One of the key notions of what it means to be dependable is verifiability, i.e., one can guarantee that the computer system does what it is supposed to do. The highest possible level of verifiability is called formal verification , which produces a mathematical proof of a system's reliability.Formal verification for hardware and software is now widely used in mission-critical real-world applications. These include the embedded code in NASA deep space probes, the arithmetic chips in Intel and AMD CPUs, and device driver code in large consumer operating systems such as Microsoft Windows. To achieve the highest level of quality assurance, formal verification is now an essential complement to testing and simulation.Formal verification relies critically on the automation of proof methods for the mathematical theories that are used to describe systems. Automated proof can be done deductively, by proceeding via composition of simple proof rules, or non-deductively, by directly exploiting our knowledge of these theories. Non-deductive proof is fast, but the reliability of deductive proof is more obvious because it can be broken up into simple pieces.In an ideal world, non-deductive proof automation programs are used as oracles for deductive ones. The difficulty is in coming up with deductive versions of the non-deductive program's answers. Achieving a clean and useful integration of non-deductive and deductive proof automation programs is a non-trivial problem.Our research looks at proofs for a relatively new but widely deployed class of non-deductive prover programs called SMT solvers . These are specialised programs for automatically proving assertions about the behaviour of computer systems, when these assertions are expressed as mathematical formulae. We plan to augment SMT solvers to allow more complex assertions to be expressed, and then to explore methods for speeding up the deductive analysis of the answers produced by SMT solvers. Both these objectives will improve the effectiveness of industrial-strength formal verification. In this endeavour we have strong support from both industry and academia. In related previous work we achieved thousands-fold speed-ups in the deductive analysis of Boolean problem solvers, for the first time making deductive verification feasible for industrial Boolean problems. We have high hopes for repeating this success. Success would mean a vastly improved capability for deductive verification, and hence the ability to provide reliable high-level quality-assurance tool kits for considerably more complicated computer systems than is currently possible.