Probabilistic CEGAR

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 arise. This paper them in the context of predicate abstraction.

• Type: Conference
• Year: 2008
• Where: CAV
• Authors: Holger Hermanns, Björn Wachter, Lijun Zhang
• Keywords: CAV 2008, Counterexample-guided Abstraction Refinement, Hardware, Predicate Abstraction, Various Foundational Questions