Li Huang

• Tests and proofs are two main techniques in modern software verification. To test a program means running the program to check if its execution yields an expected outcome. To prove a program is to build a mathematical proof, showing the correctness of the program against its desired properties. In the traditional view, however, tests and proofs are considered as two incompatible techniques. They are often treated as warring siblings and mostly applied in isolation. The complementarity of tests and proofs — though not immediately apparent — has been relatively underexplored. Can their combination mitigate each other’s weaknesses while harnessing their respective strengths? This thesis tries to straddle the border between tests and proofs and suggest a concrete answer. It explores how the two approaches can collaborate with and mutually benefit one another. Three key contributions arise from this exploration. The first contribution is Proof2Test, a framework that transforms failed proofs into useful test cases, allowing programmers to use tests to debug failed proofs effectively. The second contribution consists of several proof-based test generation strategies, which use proofs to enhance both the efficiency and effectiveness of test generation. This thesis also extends SC with “loop unrolling”, considering not just zero or one but any number of iterations, up to a set limit. It also includes an empirical study to examine how much (if anything) testing strategies miss when they limit themselves to standard branch coverage and, conversely, how many more bugs we can find if we unroll loops. The last contribution of this thesis is an automatic program repair approach, Proof2Fix, which takes advantages of the proposed test generation methods to produce meaningful corrections to faults revealed by proofs.