Verification, Testing and Statistics

摘要

Though formal verification has been the holy grail of software validation, practical applications of verification run into two major challenges. The first challenge is in writing detailed specifications, and the second challenge is in scaling verification algorithms to large software. In this short paper, we present possible approaches for these problems. We propose using statistical techniques to raise the level of abstraction, and automate the tedium in writing detailed specifications. We propose combining testing with verification to help scalability.