Collaborative Verification and Testing with Explicit Assumptions

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 correctness, 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 compensated for by complementary checkers or testing. Our experiments suggest that our technique finds more errors and proves more properties than static checking alone, testing alone, and combinations that do not explicitly document the compromises made by static checkers. Our technique is also useful to obtain small test suites for partially-verified programs.

Maria Christakis is currently in her second year as a Ph.D. student at the Chair of Programming Methodology in the Department of Computer Science of ETH Zurich, Switzerland. She is working on a technique for collaborative static checking and testing that makes compromises of static checkers explicit such that they can be compensated for by automated, specification-based testing under Peter Müller’s supervision. She received her Bachelor’s and Master’s degrees from the National Technical University of Athens, Greece. At the same university, she also worked on static and dynamic concurrency error detection in Erlang.