@inproceedings{KaufmannKPSW13,
  author    = {Petra Kaufmann and Martin Kronegger and Andreas Pfandler and Martina Seidl and Magdalena Widl},
  title     = {Global State Checker: Towards SAT-Based Reachability Analysis of Communicating State Machines},
  booktitle = {Proc. of the 10th Model-Driven Engineering, Verification, and Validation Workshop (MoDeVVa 2013) colocated with MODELS 2013},
  date      = {October 1, 2013},
  editor    = {Fr{\'e}d{\'e}ric Boulanger and Michalis Famelis and Daniel Ratiu},
  location  = {Miami, Florida},
  year      = {2013},
  month     = {October},
  pages     = {31--40},
  publisher = {},
  number    = {1069},
  series    = {CEUR Workshop Proceedings},
  abstract  = {We present a novel propositional encoding for the reachability problem of communicating state machines as provided by UML. The problem deals with the question whether there is a path to some combination of states in a state machine view starting from a given configuration. Reachability analysis finds its application in many verification scenarios. By using an encoding inspired by approaches to encode planning problems in artificial intelligence, we obtain a compact representation of the reachability problem in propositional logic. We present the formal framework for our encoding and a prototype implementation. A first case study underpins its effectiveness.}
}