https://www.dagstuhl.de/12353

28. – 31. August 2012, Event 12353

CEBug-Treffen

Organisator

Bernd Becker (Universität Freiburg, DE)

Auskunft zu diesem Event erteilt

Heike Clemens

Motivation

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

Keywords

  • Stochastic systems
  • Counterexample generation

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact aufgelistet und separat in der Bibliothek präsentiert.