Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ ZENODOarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Software
Data sources: ZENODO
addClaim

Cerisier: A Program Logic for Attestation in a Capability Machine (Artifact)

Authors: Rousseau, June; Carnier, Denis; Keuchel, Steven; Van Strydonck, Thomas; Devriese, Dominique; Birkedal, Lars;

Cerisier: A Program Logic for Attestation in a Capability Machine (Artifact)

Abstract

This is the artifact accompanying the article "Cerisier: A Program Logic for Attestation in a Capability Machine" at PLDI'26. The artifact contains the Rocq proofs accompanying the paper, built using the Iris framework. We provide The Rocq sources themselves under cerisier.tar.gz; A virtual machine cerisier.ova with a prebuilt version of the development. The VM already has Emacs and Proof General installed to explore the proofs. The project is available in the directory ~/Desktop/cerisier-artifact-pldi26 in the VM. There is no password required. Follow the instructions in the README.md, available in cerisier.tar.gz. Don't hesitate to contact us if you have any questions!

Powered by OpenAIRE graph
Found an issue? Give us feedback