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

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