TY - GEN
T1 - Probabilistic abstractions with arbitrary domains
AU - Esparza, Javier
AU - Gaiser, Andreas
PY - 2011
Y1 - 2011
N2 - Recent work by Hermanns et al. and Kattenbelt et al. has extended counterexample-guided abstraction refinement (CEGAR) to probabilistic programs. These approaches are limited to predicate abstraction. We present a novel technique, based on the abstract reachability tree recently introduced by Gulavani et al., that can use arbitrary abstract domains and widening operators (in the sense of Abstract Interpretation). We show how suitable widening operators can deduce loop invariants difficult to find for predicate abstraction, and propose refinement techniques.
AB - Recent work by Hermanns et al. and Kattenbelt et al. has extended counterexample-guided abstraction refinement (CEGAR) to probabilistic programs. These approaches are limited to predicate abstraction. We present a novel technique, based on the abstract reachability tree recently introduced by Gulavani et al., that can use arbitrary abstract domains and widening operators (in the sense of Abstract Interpretation). We show how suitable widening operators can deduce loop invariants difficult to find for predicate abstraction, and propose refinement techniques.
UR - https://www.scopus.com/pages/publications/80053094219
U2 - 10.1007/978-3-642-23702-7_25
DO - 10.1007/978-3-642-23702-7_25
M3 - Conference contribution
AN - SCOPUS:80053094219
SN - 9783642237010
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 334
EP - 350
BT - Static Analysis - 18th International Symposium, SAS 2011, Proceedings
T2 - 18th International Static Analysis Symposium, SAS 2011
Y2 - 14 September 2010 through 16 September 2010
ER -