Expressive Multi-theory Reasoning for Interactive Verification

点击翻译按钮获取中文摘要

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.