We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.SE

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Software Engineering

Title: Verifying Verified Code

Abstract: 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.
Comments: 24 pages, 17 figures, to be included in ATVA 2021 conference proceedings
Subjects: Software Engineering (cs.SE); Logic in Computer Science (cs.LO)
ACM classes: D.2.4
Cite as: arXiv:2107.00723 [cs.SE]
  (or arXiv:2107.00723v1 [cs.SE] for this version)

Submission history

From: Siddharth Priya [view email]
[v1] Thu, 1 Jul 2021 19:59:32 GMT (328kb,D)

Link back to: arXiv, form interface, contact.