We present a general framework for generating counterexamples symbolically for large discrete-time Markov chains.

We use SAT-solving techniques as well as symbolic graph algorithms.

We provide a large comparison between explicit and symbolic approaches for counterexample generation.

Our benchmarks show that we are able to generate counterexamples for systems with billions of states.