For the correction of erroneous systems it is crucial to have counterexamples at hand. Counterexamples are system runs which lead to erroneous behaviour.

Model checking for stochastic systems can be used to determine the probability with which runs of a stochastic system satisfy a given property. Unfortunately, if this probability does not lie within the admissible bounds, the available model checking algorithms cannot provide counterexamples.

The goal of the CEBug project is, on the one hand, to improve the available technologies for counterexample generation for stochastic systems and, on the other hand, to develop and implement algorithms for more expressive properties and for richer systems.

During this meeting we focus on the role of compositionality and non-determinism, and discuss the possibilities of using SAT-modulo-theories technologies for counterexample generation.

The CEBug project is financially supported by the Deutsche Forschungsgemeinschaft (DFG).