The following lists some available material related to Prosa, Coq, and ssreflect.

Setup Instructions

Coq Foundations

Prosa Documentation

As a still young project, most of the documentation is very much a work in progress. Please consider contributing to Prosa by improving and correcting the available documentation, or by asking questions on the Prosa mailing list when the existing documentation is insufficient.

Prosa Artifacts

  1. ECRTS’16 Artifact Evaluation (for Prosa v0.1): provides instructions for how to install the prerequisites, how to compile all proofs, how to check for incorrect proofs, how to enumerate all axioms, etc.

  2. Reduction-based analysis for APA Scheduling (in Prosa v0.2): provides an overview of the APA-related definitions and proofs.

  3. Self-Suspending Tasks and Weak Sustainability (in Prosa v0.3): explains the formalization of the proof of weak sustainability of the dynamic self-suspension model.

  4. Abstract Response-Time Analysis (in the completely refactored Prosa v0.4): presents the new generic framework for response-time analyses in Prosa.

Prosa Guidelines