Home Publications Tools Links Pictures

Probabilistic Model Checking Modulo Theories
with Lijun Zhang and Holger Hermanns,
Qest07   IEEE Computer Society

Abstract. Probabilistic models are widely used to analyze embedded, networked, and more recently biological systems. Existing numerical analysis techniques are limited to finite-state 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.
Download: [pdf.png]  pdf   [tex.png] bib

Links: [Google Scholar]

Chair for Programming Languages and Compiler Construction