August 28 – 31 , 2012, Event 12353



Bernd Becker (Universität Freiburg, DE)

For support, please contact

Heike Clemens


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).


  • Stochastic systems
  • Counterexample generation

Online Publications

We offer several possibilities to publish the results of your event. Please contact publishing(at) if you are interested.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf in the library.