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

Igor Konnov at FMCAD’13

Igor Konnov presented our result on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms by Abstraction at FMCAD’13 in Portland, USA.

Continue reading

Josef Widder at PODC’13

Josef Widder presented a brief announcement on Parameterized model checking of fault-tolerant distributed algorithms by abstraction at PODC’13 in Montreal, Canada.

Continue reading

Igor Konnov at SPIN’13

Igor Konnov presented our result on Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms at SPIN’13 in Stony Brook, NY, USA.

Continue reading

Igor Konnov at Dagstuhl 13141

Igor Konnov gave a talk on Parameterized Model Checking of Fault-tolerant Broadcasting Algorithms at Dagstuhl Seminar on Formal Verification of Distributed Algorithms in Dagstuhl, Germany.

Continue reading

Josef Widder in Dagstuhl

Josef Widder gave a talk on Parameterized Model Checking of Fault-tolerant Distributed Algorithms at Dagstuhl Seminar on Games and Decisions for Rigorous Systems Engineering in Dagstuhl, Germany.

Continue reading

Josef Widder at EC^2

Josef Widder told everybody on Who is afraid of Model Checking Distributed Algorithms (was it us?) at EC^2 Workshop in Berkeley, California.

Continue reading

Latest News

Helmut Veith Stipend

The first recipient of the Helmut Veith Stipend for excellent female master’s students in computer science will be presented on March 14 at the following event: "More female students in computer science. Who cares?" Panel discussion with renowned scientists about diversity in STEM Studies March 14, 5:30pm, TU Wien The Helmut Veith Stipend is dedicated […]

Continue reading

WAIT 2016 in Vienna

The third WAIT workshop on induction is held between 17-18 November at the TU Wien. Details are available on the workshop page.

Continue reading

Two papers at POPL’17

Two papers co-authored by researchers from our group have been accepted for POPL’17: “Coming to Terms with Quantified Reasoning” by Simon Robillard, Andrei Voronkov, and Laura Kovacs; and “A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms” by Igor Konnov, Marijana Lazic, Helmut Veith, and Josef Widder

Continue reading

Helmut Veith Stipend

Outstanding female students in the field of computer science who pursue (or plan to pursue) one of the master‘s programs in Computer Science at TU Wien taught in English are invited to apply for the Helmut Veith Stipend

Continue reading

Full news archive