SHF: Small: Generation of High-Quality Tests by Treating Tests as Proof Encoding

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

Verification is a bottleneck of crisis proportions in the designof the hardware and software systems society depends on. The twomain approaches to verification are formal verification andtesting. Formal verification has the advantage that it rules outthe existence of any logical bugs that violate the propertiesunder consideration. Unfortunately, current formal methods arenot scalable and cannot be directly applied to entire designs. Incontrast, testing is very scalable and is therefore the method ofchoice in practice. The disadvantage of testing is that it doesnot rule out the existence of bugs, and bugs that escape thetesting process can lead to recalls, software crashes, and eventhe loss of life. The research proposed will make testing moreeffective by developing methods of test generation that reducethe probability of missing bugs while simultaneously keeping thenumber of tests generated relatively small.The proposed research is based on the new idea that tests can bethought of as encodings of proofs. This is a fundamentallydifferent way of viewing testing, which is traditionally thoughtof as a method for sampling the space of all possible systembehaviors. The research will explore several potentiallytranformative directions. The first is that one can effectivelygenerate small and complete test sets, i.e., tests sets that ruleout the existence of bugs. Another direction is that testingregimes can be compared by checking to see which lead to testsets that are closest to encoding relevant proofs. A thirddirection is to establish strong connections that bridge the gapbetween formal verification and testing. Finally, the proposedresearch will lead to the development of efficient algorithms fortest generation that will be applied to a range of importantproblems arising in hardware and software verification.