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 algorithms are encoded in our extension of Promela by following certain code patterns (see the Spin’13 paper).

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.

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. 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

2017
[15] 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]
[14] 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]
[13] 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]
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] 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]
[2] 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]
[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 Informationssysteme 184/4
Favoritenstraße 9–11
1040 Wien
Austria

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

 

ByMC news

Paper at VMCAI’17

Our paper “Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms” is accepted at VMCAI’17

Continue reading

Artifact evaluation at POPL’17

Our artifact at POPL’17 has met the expectations of the evaluation committee (with the scores: exceeds expectations (1) + meets expectations (1)). We will upload the virtual machine soon.

Continue reading

Our paper at POPL’17

Our paper on “A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms” has been accepted to POPL 2017! Check the draft at arXiv.

Continue reading

Questions answered by Leslie Lamport

Leslie Lamport is going to answer questions about a Mathematical View of Computer Systems in Informatikhörsaal on Tuesday at 6pm. Check the announcement at the VCLA website and do not forget to watch the lecture beforehand.

Continue reading

WWTF ICT project awarded to Igor Konnov

Igor Konnov (PI), together with Josef Widder (co-PI) and Helmut Veith (core team), are awarded an ICT research project APALACHE “Abstraction-based Parameterized TLA Checker” by the Vienna Science and Technology Fund WWTF.

Continue reading

FRIDA’15

We had great talks at FRIDA’15 workshop in Grenoble. The slides of some of the talks are available online.

Continue reading

Latest News

FMSD Special Issue in Memoriam Helmut Veith

In memory of Helmut Veith, the founder of the FORSYTE research group, the current issue of the Journal on Formal Methods in System Design is a Special Issue in Memoriam Helmut Veith. Helmut unexpectedly passed away in March 2016; he was a brilliant researcher, inspiring collaborator, passionate mentor, generous friend, and valued member of the […]

Continue reading

Helmut Veith Stipend 2017: Deadline Extension (November 30)

The application deadline for the Helmut Veith Stipend 2017 has been extended to November 30. The stipend is dedicated to the memory of an outstanding computer scientist who worked in the fields of logic in computer science, computer-aided verification, software engineering, and computer security. We encourage all female master’s students attending (or planning to attend) […]

Continue reading

Helmut Veith Stipend 2017

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

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

Full news archive