Probabilistic CEGAR
Holger Hermanns‚ Björn Wachter and Lijun Zhang
Abstract
Counterexample-guided abstraction refinement (CEGAR) has been en vogue for the automatic verification of very large systems in the past years. When trying to apply CEGAR to the verification of probabilistic systems, various foundational questions and practical tradeoffs arise. This paper explores them in the context of predicate abstraction.
Book Title
CAV
Editor
Aarti Gupta and Sharad Malik
Note
Princeton‚ NJ‚ USA
Pages
162–175
Publisher
Springer Verlag
Series
LNCS
Volume
5123
Year
2008