Tools Overview Contact Us Publications Case Studies Manual Home

PASS Tool Homepage

PASS is an analysis tool for infinite-state probabilistic models. It is based on predicate abstraction and automatic abstraction refinement. Models are specified in a variant of the PRISM language. PASS computes the probability of reaching a set of goal states specified by the user.

PASS has two sisters, PARAM and INFAMY, that accept virtually the same language, but have different strengths.

Download and Installation

The latest version of PASS can be obtained here:

The version number represents the latest revision in the repository at the time the package was created.


There in no installation routine; once you have unzipped the binaries package, you can run the tool in place. If you wish, you can copy the executables to your bin directory (~/bin as normal user or /usr/bin as root to make PARAM available system-wide).


Björn Wachter and Lijun Zhang initiated the PASS project under the guidance of Professor Holger Hermanns. Beside Björn, the main developer of PASS, Lijun and Holger are key contributors. Moritz Hahn has been a very proficient co-developer (in refinement and value iteration). He siginficantly extended the frontend and has used it in his own projects.

* This work is supported by the NWO-DFG bilateral project ROCKS, by the DFG as part of the Transregional Collaborative Research Center SFB/TR 14 AVACS and the Graduiertenkolleg "Leistungsgarantien für Rechnersysteme", and has received funding from the European Community's Seventh Framework Programme under grant agreement number 214755.


For questions, comments and support requests regarding PASS, please contact "bjoern [dot] wachter [at] comlab [dot] ox [dot] ac [dot] uk". For questions regarding the PASS homepage, please contact "emh [at] cs [dot] uni [minus] saarland [dot] de".

Valid XHTML 1.1 Valid CSS! Powered by PHP