@InProceedings{HahnHWZ10,
	author={Ernst Moritz Hahn and Holger Hermanns and Bj{\"o}rn Wachter and Lijun Zhang},
	title={{PASS}: Abstraction Refinement for Infinite Probabilistic Models},
	booktitle={TACAS},
	year = {2010},
	publisher = {Springer},
        subproject = {S2,S3},
        access = {restricted},
        bibtex = {hahn.tacas10.bib},
        pdf = {hahn.tacas10.pdf},
        abstract = {We present PASS a tool that analyzes concurrent
                  probabilistic programs, which map to potentially
                  infinite Markov decision processes. PASS is based on
                  predicate abstraction and abstraction refinement and
                  scales to programs far beyond the reach of numerical
                  methods which operate on the full state space of the
                  model. The computational engines we use are SMT
                  solvers to compute finite abstractions, numerical
                  methods to compute probabilities and interpolation
                  as part of abstraction refinement. PASS has been
                  successfully applied to network protocols and serves
                  as a test platform for different refinement methods.}
}