Subproject

S2, S3

Categories

Model checker / solver for probabilistic systems

Overview

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.

Publications

E.M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. PASS: Abstraction Refinement for Infinite Probabilistic Models. In Javier Esparza and Rupak Majumdar, editors, TACAS, volume 6015 of Lecture Notes in Computer Science, pages 353-357, 2010.

B. Wachter and L. Zhang. Best Probabilistic Transformers. In Gilles Barthe and Manuel V. Hermenegildo, editors, Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 5944 of Lecture Notes in Computer Science (LNCS), pages 362-379, 2010.

H. Hermanns, B. Wachter, and L. Zhang. Probabilistic CEGAR. In Aarti Gupta and Sharad Malik, editors, Proceedings of the 20th International Conference on Computer Aided Verification, CAV 2008, volume 5123 of Lecture Notes in Computer Science (LNCS), pages 162-175, 2008.

B. Wachter, L. Zhang, and H. Hermanns. Probabilistic Model Checking Modulo Theories. In Proceedings of the Fourth International Conference on the Quantitative Evaluation of Systems, 2007.

Benchmarks

See depend.cs.uni-saarland.de/tools/pass/casestudies/

Download

See depend.cs.uni-saarland.de/tools/pass/

Manual

See depend.cs.uni-saarland.de/tools/pass/manual/

Status

Stable