Campus Event Calendar

Event Entry

New for: D3

What and Who

Testing a Verification Environment

Markus Wagner
University of Koblenz -Landau
PhD Application Talk
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
Public Audience

Date, Time and Location

Tuesday, 16 February 2010
90 Minutes
E1 4


The goal of software verification is the proof of correctness of a program with respect to its specification. Normally, the tools used in a verification process are not verified, and their correctness is taken for

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.


IMPRS-CS Office Team
0681 - 93 25 225
--email hidden
passcode not visible
logged in users only

Tags, Category, Keywords and additional notes

Stephanie Jörg, 02/12/2010 12:08 -- Created document.