Towards Testing a Verifying Compiler

Thorsten Bormer and Markus Wagner


In this paper, we present our approach on testing a particular verification 
system that is industrially used to generate mathematical proofs of the 
correctness of C programs. 
Normally, the tools used in such a verification process are seldomly 
verified nor thoroughly tested, and their correctness is taken for granted.
Our approach to obtain assurance in such tools does not rely on the 
knowledge of their internal details and enables regular users of these tools
to write test cases for them. Those tests are then assessed using our 
domain-specific "axiomatization coverage" that measures the impact of the 
axiomatization, which is an integral component of the verification process. 
Furthermore, we explore several sources of test cases, as the risk of 
constructing buggy test cases is high due to the input domain's complexity.