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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element