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 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.
@article{arxiv.2107.00723,
title = {Verifying Verified Code},
author = {Siddharth Priya and Xiang Zhou and Yusen Su and Yakir Vizel and Yuyan Bao and Arie Gurfinkel},
journal= {arXiv preprint arXiv:2107.00723},
year = {2021}
}
Comments
24 pages, 17 figures, to be included in ATVA 2021 conference proceedings