Dara: hybrid model checking of distributed systems

Abstract

Building correct implementations of distributed systems continues to elude us. Solutions consist of abstract modeling languages such as TLA+, PLusCal, which specify models of systems and tools like Coq, and SPIN which verify correctness of models but require considerable amount of effort, or transparent model checkers like MODIST, CMC and CHESS which suffer from state space explosion, rendering them impractical to use as they are too slow.

BibTeX

@inproceedings{Anand:FSE18,
  author    = {Vaastav Anand},
  title     = {Dara: hybrid model checking of distributed systems},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {977--979},
  publisher = {{ACM}},
  year      = {2018},
}

Dara: hybrid model checking of distributed systems

Abstract

Related papers