Formal Methods Tools

At a Glance

Applications Probabilistic Abstraction
Developers Saarland University
Inputs PRISM
Interfaces CLI
Licenses All Rights Reserved
Maintenance Not Maintained

Description

[ Not Maintained Since 2010 ]
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.