Model-Checking the Implementation of Consent (Accompanying Artifact)

This artifact contains the TLA+ mechanization of the PILOT semantics and refinements (program graphs) introduced in the submitted paper "Model-Checking the Implementation of Consent". The main contribution of this artifact is the TLA+ code itself that serves as a demonstration on how to define refinements (implementations) of the PILOT abstract semantics. The artifact also includes the necessary software to model-check the privacy requirements and refinements described in the paper. The TLA+ source code in this artifact is also publicly available at https://github.com/raulpardo/pilot-tla.