Generating Regression Unit Tests using a Combination of Verification and Capture & Replay Bernhard Beckert, Christoph Gladisch, Shmuel Tyszberowicz,Amiram Yehudai Recently the combination of software verification and testing techniques is increasingly encouraged due to their complementary strenghs. Some verification tools have extensions for test case generation. These tests are strong at detecting software faults during the implementation and verification phase, and to further increase the confidence in the final software product. However, tests generated using verification technology alone may lack some of the benefits obtained by using more traditional testing techniques. One such technique is Capture and Replay whos strenghts are the generation of isolated unit tests and regression test oracles. We identified that the two groups of techniques have complementary strengths, and therefore are ideal candidates for a tool-chain approach proposed in this paper. The first phase produces, for a given system, unit tests with high coverage. However, when using them to test a unit, its environment is tested as well - resulting in a high cost of testing. To solve this problem, the second phase captures the various executions of the program, which are monitored by the output of the first phase. The output of the second phase is a set of unit tests with high code coverage, which use mock objects to test the units. Another advantage of the proposed approach is the fact that the generated tests can also be used for regression testing.