Verifying Verified Code
This is an incremental study that addresses verification methodology for industry code, potentially improving specification reuse and tool interoperability.
The paper investigates three research questions about bounded model checking methodology by porting verification tasks for the aws-c-common library to SEAHORN and KLEE, showing benefits of compiler semantics and cross-checking specifications.
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow up case study that explores the methodology from the perspective of three research questions: (a) can proof artifacts be used across verification tools; (b) are there bugs in verified code; and (c) can specifications be improved. To study these questions, we port the verification tasks for $\texttt{aws-c-common}$ library to SEAHORN and KLEE. We show the benefits of using compiler semantics and cross-checking specifications with different verification techniques, and call for standardizing proof library extensions to increase specification reuse. The verification tasks discussed are publicly available online.