2011/06/07 by Javier Esparza, Esparza, Javier, Andreas Gaiser +1
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1106.1364
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 diffcult to find for predicate abstraction, and propose refinement techniques.