V.: Collaborative verification and testing with explicit assumptions

Abstract. Many mainstream static code checkers make a number of compromises to improve automation, performance, and accuracy. These compromises include not checking certain program properties as well as making implicit, unsound assumptions. Consequently, the results of such static checkers do not provide definite guarantees about program correct-ness, which makes it unclear which properties remain to be tested. We propose a technique for collaborative verification and testing that makes compromises of static checkers explicit such that they can be compen-sated for by complementary checkers or testing. Our experiments sug-gest that our technique finds more errors and proves more properties than static checking alone, testing alone, and combinations that do not explic-itly document the compromises made by static checkers. Our technique is also useful to obtain small test suites for partially-verified programs.