ByMC: Byzantine Model Checker

bymc

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

  • 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

© Sara MeisterMarijana Lazić

igor konnov

Igor Konnov

Josef Widder, (c) Sebastien TixeuilJosef Widder

Annu GmeinerAnnu Gmeiner

Events

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

Publications

2020
[20] Tutorial: Parameterized Verification with Byzantine Model Checker
Igor Konnov, Marijana Lazic, Ilina Stoilkovska, Josef Widder
FORTE 2020, pages 189–207, 2020.
[bibtex] [pdf]
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.

Contact

Address:
Igor Konnov
Technische Universität Wien
Institut für Logic and Computation 192/4
Favoritenstraße 9–11
1040 Wien
Austria

Room: HD 03 13 (how to get there)
Phone: +43 (1) 58801 – 184 807
Email: konnov@forsyte.at
Web: http://forsyte.at/~konnov/

ByMC news

Apologies, but no results were found.

Latest News

Winter School on Verification

The Austrian Society for Rigorous Systems Engineering (ARiSE) and the Vienna Center for Logic and Algorithms (VCLA) are organizing a joint winter school on verification at Vienna University of Technology from 6-10 February 2012. Apart from ARiSE/VCLA students, the school will be open to outside students. Details are available from the VCLA website.

Continue reading

CfP: Workshop on Exploiting Concurrency Efficiently and Correctly (EC^2 2010)

The annual Workshop on Exploiting Concurrency Efficiently and Correctly (EC2) is a forum that brings together researchers working on formal methods for concurrency, and those working on advanced parallel applications. Its goal is to stimulate incubation of ideas leading to future concurrent system design an verification tools that are essential in the multi-core era.

Continue reading

Full news archive