Artifact: Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows

This artifact (the Docker Image) contains the following components: our tools (CN, Fulminate, and Darcy), verification results for the pKVM hyp allocator, and an Android Linux with the instrumented hyp allocator. For the most up-to-date versions, refer to the following repositories: CN, Fulminate, and Darcy Cut-out hyp allocator with specifications and proofs Fulminate-Instrumented Android Linux NOTE: the authors of the repository given above are the authors of the paper "Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows", for which this repository contains additional materials. For information about authors and license of the source code, see the uploaded files. For instructions on how to use this artifact, please see README.md included in the artifact.