Verification-Preserving Inlining in Automatic Separation Logic Verifiers -- Artifact

This includes the artifact submitted to the OOPSLA 2023 artifact evaluation committee for the paper "Verification-Preserving Inlining in Automatic Separation Logic Verifiers" We have installed all required dependencies on an Ubuntu 20.04 VirtualBox virtual machine. To test the artifact, we used 8 GB of RAM (using less RAM can lead to problems when checking proofs with Isabelle) and 2 processors for the virtual machine and VirtualBox version 6.1. The username is “inlining” and the password is “test”. The README for the artifact is provided as a pdf (readme_artifact_inlining.pdf). Moreover, there is a pdf (dual_inlining_result_proof.pdf) that contains the proof of a dual result that is mentioned in the paper: successful verification of the inlined program ensures that there are method and loop annotations that enable the verification of the original program for bounded executions. This dual result was not part of the artifact evaluation