Testing a Verification Environment

granted. One approach to check the quality of these tools without verifying them is by testing.

In the BMBF-project "Verisoft XT", the Verifying C Compiler (VCC) from Microsoft Research is used for the verification of C code. It is impossible to come up with a correctness proof of VCC’s sound functioning and to keep it up-to-date because of two reasons. First, VCC is being developed during the project, which results in frequent changes of the implementation and the verification formalism. Second, the compiler is used as a black box for nonexperts.

The goal of this thesis is to develop a systematic testing process for blackbox verification systems. The theoretical part consists of the application of the concepts of black-box software testing in the context of verification systems. This includes the definition of the subject under test and the definition of a suitable test metric. This process is applied to VCC, resulting in a specialized test suite and a test harness. The test harness will run and monitor the tests without user interaction, enabling the regression testing of both VCC and an arbitrary code base.