SHF: Small: Incremental Inductive Verification: A New Direction for Model Checking

硬件和软件计算机系统集成到我们社会的许多方面，包括医疗，交通，金融市场和通信。 因此，计算机系统的正确性对于财务或甚至人类安全原因而言是至关重要的。形式验证是一种发现错误并证明系统没有错误的方法。 它补充了测试，在实践中，测试既不能涵盖所有可能性，也不能宣布没有错误。 由于近年来计算机系统的日益复杂和普及，形式验证算法的显著改进现在对计算机系统开发产生了直接影响，这反过来又降低了设计成本，加快了开发速度，并导致更安全的设备。本项目建立在用于验证数字硬件不变性的IC3算法的成功基础上。 IC3仅在两年前推出，已经被硬件制造商和电子设计自动化公司广泛使用。 据报道，在实践中，它可以发现测试难以发现的深层错误，或者获得其他算法无法找到的证明。 但是，要实现下一个显著的性能提升，需要超越IC3执行的位级分析，而是考虑字级设计，即有时考虑整个寄存器而不仅仅是其组件锁存器的设计。 该项目通过开发IC3的多域版本以及抽象域来解决这一挑战，用于推理等式，未解释的函数和电路的算术属性。 该项目的第二个组成部分是扩展增量归纳验证（IIV）方法，其中IC3是第一个实例，以分析CTL和CTL* 中表达的属性，CTL和CTL* 是用于表达分支时间行为的逻辑。 增强的表现力允许分析设计的更多方面。 最后一个组件是通过分布式实现来利用IIV算法的自然并行性。

Hardware and software computer systems are integrated into many aspects of our society, including medicine, transportation, financial markets, and communication. Thus, the correctness of a computer system can be critical for financial or even human safety reasons. Formal verification is a methodology for finding errors and certifying that a system is free of errors. It complements testing, which in practice can neither cover every possibility nor declare the absence of errors. Because of the increasing complexity and prevalence of computer systems in recent years, significant improvements in algorithms for formal verification now have an immediate impact in computer system development, which in turn decreases design costs, accelerates development, and results in safer equipment.This project builds on the success of the IC3 algorithm for verifying invariance properties of digital hardware. IC3, introduced only two years ago, is already used widely by hardware manufacturers and electronic design automation companies. It is reported that it can, in practice, find deep bugs that are difficult to find with testing, or obtain proofs that no other algorithm can find. But achieving the next significant gain in performance requires moving beyond the bit-level analysis that IC3 performs and instead considering designs at the word level, that is, at a level in which whole registers are sometimes considered rather just than their component latches. This project addresses this challenge by developing a multi-domain version of IC3, as well as abstract domains, for reasoning about equality, uninterpreted functions, and arithmetic properties of circuits. A second component of this project is to extend the incremental, inductive verification (IIV) methodology, of which IC3 was the first instance, to analyze properties expressed in CTL and CTL*, which are logics for expressing branching-time behavior. Increased expressiveness allows analyzing more aspects of a design. A final component is to exploit the natural parallelism of IIV algorithms through a distributed implementation.