Probabilistic models are widely used to analyze embedded, networked, and more recently biological systems. Existing numerical analysis techniques are limited to finitestate models and suffer from the state explosion problem. As a consequence, the user often has to manually abstract the intended model to get a tractable one. To this end, we propose the predicate abstraction model checker PASS which automates this process. We leverage recent advances in automatic theorem proving to compute tractable finite-state models. Experiments show the feasibility of our approach. To the best of our knowledge, this is the first time that properties of probabilistic infinite-state models have been verified at this level of automation.