The Integration of Testing and Program Verification: A Position Paper

Formal analysis techniques for software systems are becoming more and more powerful, and have been used on non-trivial examples. We argue that the next step forward is to combine these different techniques in a single framework, which makes it possible to (i) analyse different parts of the system with different techniques, (ii) apply different techniques on a single component, and (iii) seamlessly combine the results of the various analysis. We describe our vision of how this integration can be achieved for the analysis techniques of testing and deductive verification. We end with an overview of research challenges that need to be addressed to achieve this vision