Improving test coverage of formal verification systems via beam search

Abstract

The correctness of program verifcation systems is of great importance, since they are used to formally prove that safety- and security-critical programs follow their specifcation. Within these verifcation systems, the background axiomatization captures the semantics of the target program language|errors here can lead to incorrect formal proofs, which in turn can have devastating consequences. Testing the axiomatization thoroughly is one approach to increase the trust in its correctness, however, the manual creation of test cases is a very time-consuming process for verifcation engineers. We present a beam search approach for creating test cases through test case modifcations.