Automated Test Generation And Verified Software?

Abstract. Testing remains the principal means of verification in many certification regimes. Formal methods of verification will coexist with testing and should be developed in ways that improve, supplement, and exploit the value of testing. I describe automated test generation, which uses technology from formal methods to mechanize the construction of test cases, and discuss some of the research challenges in this area. 1 Introduction By testing I mean observation of a program in execution under controlled condi-tions. Observations are compared against an explicit or informal oracle to detect bugs or confirm correctness. Much of the testing process is automated in mod-ern development environments, but construction of test cases (i.e., the specific experiments to be performed) remains a largely manual process. Testing is the method by which most software is verified today. This is truefor safety critical software as well as the commodity variety: the highest level o