This repository contains our artifacts for the paper "Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification".
It contains the following:
- developed-unit-proofs: This directory contains the unit proofs developed for each embedded operating system evaluated in the paper.
- data-and-scripts: This directory contains the raw data and the scripts used to answer each research question.
- reintroduced-defects: This directory contains the repositories for the embedded OS projects and the corresponding defects reintroduced in them.
- new-defects-found: This directory contains details of the new defects found in the respective embedded software projects. We include the detailed reports we submitted to the corresponding project maintainers.
- unit-proofing-strategies: This directory contains a compilation of the strategies applied to resolve unit proofing errors. It will help engineers easily resolve similar challenges during unit proofing.
The README files in the different directories provide details of the content and structure of these directories.