ByMC: Byzantine Model Checker

ByMC is a toolset for parameterized model checking of threshold-guarded fault-tolerant distributed algorithms (check our benchmarks for example). The most recent discussion of the tool can be found in the the paper at ISOLA’18.

Tutorial: Check the tutorial on running the tool and understanding the output.

The most recent and efficient techniques can be found in our CAV’15 paper (limited to reachability properties) and POPL’17 paper (safety and liveness). To get an overview of the implemented techniques, read our PSI’15 paper called “What you always wanted to know about model checking of fault-tolerant distributed algorithms“. A detailed exposition of the earlier techniques can be found in the tutorial given at SFM Summer School’14. Older case studies were encoded in our extension of Promela by following certain code patterns (see the Spin’13 paper). Recent case studies are encoded directly encoded in threshold automata. Check the paper at ISOLA’18.

Benchmarks and source code

The master branch of ByMC is available at github. Browse up-to-date benchmarks in the benchmarks repository.

Downloads

17.11.2018, ver. 2.4.2 (submission 82 + ISOLA18). Virtual machine (Debian 9 64bit): bymc-2.4.2.ova [2.0 GB]. For details, submission 82 and the ISOLA18 paper.
29.09.2017, ver. 2.2.1 (FMSD17) + ver. 2.4.0 (submission to OPODIS17). Virtual machine (Debian 8 64bit): bymc-2.4.0-fmsd17-and-opodis17-submission3-64bit.ova. For details, see OPODIS17 artifact description.
16.01.2017, ver. 2.2.0 Virtual machine (Debian 8u1 64-bit) improved after the POPL’17 artifact evaluation: bymc-2.2.0-popl17-64bit.ova [1.6 GB]. For details, see POPL17 artifact description.
16.01.2017, ver. 2.2.0: Source code: bymc-2.2.0-src.tar.bz2 [218 KB]
12.07.2015 Virtual machine (Debian 8.0 64-bit) brewed according to the CAV artifact evaluation guidelines and improved after the artifact evaluation: cav15-198-64bit.ova [1.2 GB]
25.04.2015: Virtual machine (Slitaz Linux) brewed according to the CAV artifact evaluation guidelines: cav15-artifact.ova [375 MB]
08.02.2015, ver. 0.9.5: Virtual machine (Slitaz Linux): bymc-0.9.5-submission198.ova [411 MB]
08.02.2015, ver. 0.9.5: Source code: bymc-0.9.5-20150208-submission198.tar.bz2 [171 KB]
24.10.2014, ver. 0.6.7: Virtual machine (Slitaz Linux): bymc-0. 6.7-luxemburg14-rc2.ova [254 MB]

24.10.2014, ver. 0.6.7: Source code: bymc-src- luxemburg14-rc2.tar.bz2 [1.1 MB]

15.06.2014, ver. 0.6.5: Virtual machine(Slitaz Linux): bymc0.6.5-slitaz5- sfm14.ova [242 MB]
20.04.2014, ver. 0.6.5: Source code: bymc-src-0.6.5 -20140420.tar.bz2 [1.1 MB]

13.09.2013, ver. 0.1.2: Source code: bymc-0.1.2-src.tar .bz2 [128 KB]

23.10.2013, ver. 0.1.2: Virtual machine(Slitaz Linux): bymc-0.1.2-vm.ova [264 MB] (it is ancient!)

To see the tool running, download and compile the source code in OCaml as written in README.txt. If, however, compiling the OCaml code and trying to meet all dependencies is too tedious, download a snapshot of a virtual machine with pre-installed Linux, the binary distribution of ByMC, and the examples in Promela and threshold automata. Install Oracle VirtualBox first and then import the virtual machine.

People

Events

See the short list on the right or check the full archive.

Publications

2018
[19]	ByMC: Byzantine Model Checker Igor Konnov, Josef Widder Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, pages 327-342, 2018, Springer International Publishing. [bibtex] [pdf] [doi]
[18]	Reachability in Parameterized Systems: All Flavors of Threshold Automata Jure Kukovec, Igor Konnov, Josef Widder 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, pages 19:1-19:17, 2018. [bibtex] [pdf] [doi]
2017
[17]	Synthesis of Distributed Algorithms with Parameterized Threshold Guards Marijana Lazic, Igor Konnov, Josef Widder, Roderick Bloem OPODIS, volume 95 of LIPIcs, pages 32:1-32:20, 2017. [bibtex] [pdf]
[16]	Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347-366, 2017. [bibtex] [pdf] [doi]
[15]	On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability Igor V. Konnov, Helmut Veith, Josef Widder Inf. Comput., volume 252, pages 95-109, 2017. [bibtex] [pdf] [doi]
[14]	A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 719-734, 2017. Note: A pre-print including the proofs is available at http://arxiv.org/abs/1608.05327 [bibtex] [pdf]
[13]	Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder Formal Methods in System Design, volume 51, number 2, pages 270-307, 2017, Springer. [bibtex] [pdf]
2016
[12]	What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms Igor Konnov, Helmut Veith, Josef Widder Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (Manuel Mazzara, Andrei Voronkov, eds.), volume 9609 of LNCS, pages 6-21, 2016, Springer International Publishing. [bibtex] [pdf]
[11]	A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder arXiv/CoRR, volume 1608.05327, 2016. Note: (accepted to POPL 2017) [bibtex] [pdf]
2015
[10]	Challenges in Model Checking of Fault-tolerant Designs in TLA+ Igor Konnov, Helmut Veith, Josef Widder 2015, Presentation at the 8th International Workshop on Exploiting Concurrency Efficiently and Correctly, San Francisco, CA, USA, July. [bibtex] [pdf]
[9]	SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms Igor Konnov, Helmut Veith, Josef Widder CAV (Part I), volume 9206 of LNCS, pages 85-102, 2015. [bibtex] [pdf]
2014
[8]	On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability Igor Konnov, Helmut Veith, Josef Widder Chapter in CONCUR 2014 --- Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 125-140, 2014. [bibtex] [pdf]
[7]	Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms Annu Gmeiner, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder Formal Methods for Executable Software Models, pages 122-171, 2014, Springer. [bibtex] [pdf]
2013
[6]	Parameterized model checking of fault-tolerant distributed algorithms by abstraction Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder FMCAD, pages 201-209, 2013. [bibtex] [pdf]
[5]	Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder SPIN, volume 7976 of LNCS, pages 209-226, 2013. [bibtex] [pdf]
[4]	Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder PODC, pages 119-121, 2013. [bibtex] [pdf]
2012
[3]	Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder ArXiv e-prints, October 2012. [bibtex] [pdf]
[2]	Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder ArXiv e-prints, October 2012. [bibtex] [pdf]
[1]	Who is afraid of Model Checking Distributed Algorithms? Igor Konnov, Helmut Veith, Josef Widder 2012, Presentation at the CAV Workshop (EC)^2. [bibtex] [pdf]

How to use the virtual machine?

Import a virtual machine (check the manual on importing), start it, log in with name ‘user’ and password ‘user’, run Terminal, change directory to ~/bymc/bymc and run one of the verify-* scripts. For details, check with ~/bymc/bymc/README.txt. You can find the benchmarks in ~/benchmarks.