Prosa and ProBsa • The Bozhko26 Editions

The Bozhko26 Edition is the version of Prosa discussed by Sergey Bozhko in his dissertation. Additionally, this page also provides the corresponding version of his ProBsa library for the mechanized analysis of probabilistic real-time systems.

Download

Download the full source code here:

• prosa-Bozhko26.tar.bz2
• probsa-Bozhko26.tar.bz2

Reading Prosa

The Bozhko26 edition of Prosa uses CoqdocJS to obtain a prettier rendering of the spec with folded proofs.

• Read the Prosa specification with folded proofs (recommended for interactive use).

Alternatively, there is also a plain coqdoc version without proofs (which is better suited for printing to PDF).

• Read the Prosa specification without proofs.

Reading ProBsa

ProBsa uses plain coqdoc output and is thus easiest to read with all proofs elided:

• Read the ProBsa specification without proofs.

Alternatively, a rendering with all proofs is also available:

• Read the ProBsa specification with proofs.