Verification is currently a major bottleneck in the design of the hardware and software systems society depends on. Design errors can lead to recalls, software crashes, cyber attacks, and even the loss of life. A fundamental approach for identifying and fixing design errors is to use formal verification, which checks whether a set of system properties holds across all possible system behaviors. Unfortunately, current algorithms suffer from poor scalability and cannot be directly applied to modern designs. This drawback is currently addressed with the use of manual abstractions that in essence hide irrelevant implementation details, thereby reducing the size of formulas to be analyzed. Besides the manual effort involved, another disadvantage of this approach is that it is very hard to guarantee that an abstraction is correct. The goal of the proposed research is to develop efficient methods for algorithmically building provably correct abstractions, thereby drastically improving the scalability of formal verification algorithms.
Our approach to finding correct abstractions is based on the following three ideas. First, building an abstraction that is correct in a small subspace of the search space is easy. Second, one can stitch together abstractions found for subspaces to produce an abstraction for the entire subspace explored so far. Third, abstractions built for explored subspaces may hold in many subspaces that have not been visited yet. This re-usability of abstractions makes our approach extremely powerful in identifying irrelevant parts of formulas. From a theoretical point of view, the proposed research will lead to a better understanding of abstractions and to the development of new formal verification algorithms. From a practical point of view, it will result in the creation of various kinds of tools including SAT-solvers and model checkers that will boost the scalability of formal verification.
