This website and associated GitHub Repository https://github.com/verus-lang/paper-sosp24-artifact contain the artifact for the paper:

Verus: A Practical Foundation for Systems Verification

Andrea Lattuada (MPI-SWS), Travis Hance (Carnegie Mellon University), Jay Bosamiya (Microsoft Research), Matthias Brun (ETH Zurich), Chanhee Cho (Carnegie Mellon University), Hayley LeBlanc (University of Texas at Austin), Pranav Srinivasan (University of Michigan), Reto Achermann (University of British Columbia), Tej Chajed (University of Wisconsin-Madison), Chris Hawblitzel (Microsoft Research), Jon Howell (VMware Research), Jacob R. Lorch (Microsoft Research), Oded Padon (Weizmann Institute of Science), Bryan Parno (Carnegie Mellon University)
The current paper draft (in shepherding) is at assets/paper-20240921-162720-b7db935.pdf

Artifact Guide

The artifact guide (guide.html) contains instructions to reproduce the results in the paper.

Case Studies

The case studies used in the paper are open-source and listed on the case studies page (case-studies.html).

External Repositories

This artifact references external repositories with open-source versions of Verus and the use cases presented. The artifact uses fixed commits (or "refspecs" / SHAs) which are also listed here: https://github.com/verus-lang/paper-sosp24-artifact/blob/main/external-repository-versions.md.

Reusability of Millibenchmark programs

The programs used for Millibenchmarks are in the milli/ directory. Some are adapted from existing open source examples or projects, typically from one of the other verifiers' examples.

If you would like to reuse these programs for further evaluation or to improve tooling, refer to the files in linked-list and doubly-linked-list with the name corresponding to the tool.
These are the programs used for Figure 7a.

Programs for the memory reasoning benchmark (Figure 7b) are generated with the `repeat*py` scripts, while programs for evaluating verification time of finding errors (Figure 8) are adapted from the linked list programs by removing necessary preconditions: these are in linked-list/errors.

At the time of paper submission Creusot required interactive sessions in the Why3 prover environment. These have been stored in creusot-* directories in linked-list, linked-list/errors, and doubly-linked-list.