Probabilistic Verifier (ProVer)

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

Source code: GZIP (version 1.1; September 10, 2002)

Publications

• 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.

Håkan L. S. Younes
Last modified: Sat Jun 24 19:48:31 EDT 2006