**ProVer is outdated. Take a look at Ymer
instead.**

ProVer implements the model independent verification algorithm proposed by Younes & Simmons (2002) for verifying probabilistic real-time properties of discrete event systems through the use of acceptance sampling. Properties are expressed using the continuous stochastic logic (CSL), and discrete event systems are specified using a stochastic process definition language (SPDL) inspired by PDDL. SPDL is expressive enough to allow the specification of time-homogeneous generalized semi-Markov processes (GSMPs).

ProVer is written in C++, and has been reported to compile on the following systems:

- Digital UNIX 4.0
- RedHat Linux 5.2, 6.2, 7.0, 7.1
- IRIX 6.5
- SunOS 5.5, 5.7

Released versions of ProVer can be downloaded here.

Håkan L. S. Younes and Reid G. Simmons. 2002. Probabilistic verification of discrete event systems using acceptance sampling. In

*Proceedings of the 14th International Conference on Computer Aided Verification*, edited by Ed Brinksma and Kim Guldstrand Larsen, vol. 2404 of*Lecture Notes in Computer Science*, 223–235, Copenhagen, Denmark. Springer.