Verification is a bottleneck of crisis proportions in the design of the hardware and software systems society depends on. The two main approaches to verification are formal verification and testing. Formal verification has the advantage that it rules out the existence of any logical bugs that violate the properties under consideration. Unfortunately, current formal methods are not scalable and cannot be directly applied to entire designs. In contrast, testing is very scalable and is therefore the method of choice in practice. The disadvantage of testing is that it does not rule out the existence of bugs, and bugs that escape the testing process can lead to recalls, software crashes, and even the loss of life. The research proposed will make testing more effective by developing methods of test generation that reduce the probability of missing bugs while simultaneously keeping the number of tests generated relatively small.
The proposed research is based on the new idea that tests can be thought of as encodings of proofs. This is a fundamentally different way of viewing testing, which is traditionally thought of as a method for sampling the space of all possible system behaviors. The research will explore several potentially tranformative directions. The first is that one can effectively generate small and complete test sets, i.e., tests sets that rule out the existence of bugs. Another direction is that testing regimes can be compared by checking to see which lead to test sets that are closest to encoding relevant proofs. A third direction is to establish strong connections that bridge the gap between formal verification and testing. Finally, the proposed research will lead to the development of efficient algorithms for test generation that will be applied to a range of important problems arising in hardware and software verification.
