ByMC: Byzantine Model Checker

This is a toolset for parameterized model checking of threshold-guarded fault-tolerant distributed algorithms.

Status

The tool author Igor Konnov is not developing it anymore. If you want to see new cool projects, check Quint and Apalache.

Publications

A recent survey of the techniques implemented in ByMC (and other tools) can be found in the paper at LMCS'23:

Igor Konnov ; Marijana Lazić ; Ilina Stoilkovska ; Josef Widder -
Survey on Parameterized Verification with Threshold Automata and the
Byzantine Model Checker. Logical Methods in Computer Science, January 18,
2023, Volume 19, Issue 1

Follow the references in the survey to learn more about the older techniques.

Installation

WARNING: Since this tool is using libraries that go back to 2013, it is getting harder to compile it. The easiest way to run ByMC is by downloading a virtual machine and running the tool inside VirtualBox. The latest version is ByMC 2.4.4 (at Google Drive).

Next steps

• To see the tool in action, read the tutorial.
• For installation instructions, check README in the source directory.
• To see the accompanying publications, visit the tool website.

Structure

The directory layout is as follows:

• bymc -- the scripts and tool source code

• plugins -- tool plugins

• legacy-bddc -- set of auxiliary scripts for model checking with NuSMV, needed only to run legacy techniques

• legacy-deps -- various dependencies required by the tools that are hard to install automatically, needed only to run legacy techniques