cid 7c758d46b783c88a8ffc54f9e1b1ccef750bb6015db92a2c38c2a005ce9e3f7b · original · open access · via openalex
Title: ProofPulse: Interactive Proof Coverage Analysis for Dafny (Artifact) Authors: Silva Álvaro; Martins Ruben; Mendes Alexandra Venue: Zenodo (CERN European Organization for Nuclear Research) Year: 2026 Canonical: doi:10.5281/zenodo.21174685 URL: https://doi.org/10.5281/zenodo.21174685 Collector: openalex OA: true ABSTRACT # Artifact Abstract ## 1. Paper title ProofPulse: Interactive Proof Coverage Analysis for Dafny ## 2. Link to the accepted paper Submitted directly on the platform Note: The paper submitted for the Artifact Evaluation track contains updated results compared to the accepted version. These results will be incorporated into the camera-ready paper. Therefore, it is best to use the paper submitted to the Artifact Evaluation track, as its results match the provided artifact. ## 3. Purpose ProofPulse is a Dafny proof-dependency and coverage analysis tool. It parses prover logs, constructs a proof graph, computes line-level coverage, and presents the result in a browser viewer and a VS Code extension. The artifact supports the paper’s claims about proof coverage analysis, diagnosis of weak proofs, and the effect of unsat-core minimization on coverage attribution. ## 4. Badge The artifact is being submitted for the following badges: * **Available**: the artifact is hosted on a public archival repository with a DOI. The source is also publicly accessible on GitHub (https://github.com/VeriFixer/ProofPulse) under an open-source license. * **Reusable**: the artifact is structured for repurposing beyond paper reproduction. The core analysis library (`@proofpulse/core`) is a standalone npm package with a clean public API, usable as a library or via CLI on any Dafny program. The architecture is modular (log parser, proof graph, coverage engine) and documented so that each component can be extended or replaced independently. The analysis pipeline is language-agnostic at the graph level — any verification-aware language producing a compatible log format can reuse the coverage engine without modification. The repository includes a full test suite with annotated oracles and YAML snapshot tests, a CI pipeline for automated regression checking, demo examples, benchmark scripts, and a web viewer — all enabling reviewers and future researchers to understand, modify, and extend the tool. * **Functional**: the artifact is documented (README with getting-started and step-by-step instructions), consistent (results match the paper tables), complete (all paper claims are reproducible), and exercisable (Docker image with smoke test completing in under 10 minutes). It includes verification and validation evidence: a 60+ case test suite under `dataset/tests/` with per-line coverage oracles and full proof-graph snapshot assertions, executed automatically via GitHub Actions CI on every commit. ## 5. Technology ### Assumed reviewer skills * Basic command-line usage. * Basic familiarity with Docker. * Basic familiarity with Dafny verification concepts. * Basic familiarity with VS Code for the editor integration. ### Hardware and software requirements * Operating system: Linux is the primary target. * Architectures: x86-64 was tested. * GPU: not required. * Docker 24 or newer is recommended for the review workflow. * At least 8 GB RAM and roughly 10 GB of free disk space are recommended. ## 6. Provenance The artifact can be obtained from this repository and its packaged review distribution. * Source Public repository: https://github.com/VeriFixer/ProofPulse ## 7. Instructions **Prerequisite:** Docker must be installed on your system. See the [official Docker installation guide](https://docs.docker.com/get-docker/) for instructions.### Getting started 1. Load the provided Docker image archive. ```bash docker load -i proofpulse-dev.tar.gz ``` 2. Start the container. ```bash docker run -it -p 8080:8080 --entrypoint bash proofpulse-dev ``` Note: If port 8080:8080 is already in use, try a different host port like 8081:8080 (if you change the port, use the same one when opening localhost in your browser) (if you change the port you will have to use the same when opening on the localhost) After running docker run, you should be in a Docker shell, where you can follow the instructions in README.md. And you can also inspect the original Dockerfile (Dockerfile devenv) used to generate this image, which lists all ProofPulse dependencies. Also, the README.md, REQUIREMENTS, STATUS, LICENSE present alongside the Docker image tar.gz are also inside the Docker image (And the instructions there assume you are already inside the image).