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 Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, pages 327-342, 2018, Springer International Publishing. |
| [18] | Reachability in Parameterized Systems: All Flavors of Threshold Automata 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, pages 19:1-19:17, 2018. |
| 2017 | |
| [17] | Synthesis of Distributed Algorithms with Parameterized Threshold Guards OPODIS, volume 95 of LIPIcs, pages 32:1-32:20, 2017. |
| [16] | Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347-366, 2017. |
| [15] | On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability Inf. Comput., volume 252, pages 95-109, 2017. |
| [14] | A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms 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 |
| [13] | Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms Formal Methods in System Design, volume 51, number 2, pages 270-307, 2017, Springer. |
| 2016 | |
| [12] | What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms 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. |
| [11] | A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms arXiv/CoRR, volume 1608.05327, 2016. Note: (accepted to POPL 2017) |
| 2015 | |
| [10] | Challenges in Model Checking of Fault-tolerant Designs in TLA+ 2015, Presentation at the 8th International Workshop on Exploiting Concurrency Efficiently and Correctly, San Francisco, CA, USA, July. |
| [9] | SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms CAV (Part I), volume 9206 of LNCS, pages 85-102, 2015. |
| 2014 | |
| [8] | On the Completeness of Bounded Model Checking for Threshold-Based Distributed Algorithms: Reachability Chapter in CONCUR 2014 --- Concurrency Theory (Paolo Baldan, Daniele Gorla, eds.), volume 8704 of Lecture Notes in Computer Science, pages 125-140, 2014. |
| [7] | Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms Formal Methods for Executable Software Models, pages 122-171, 2014, Springer. |
| 2013 | |
| [6] | Parameterized model checking of fault-tolerant distributed algorithms by abstraction FMCAD, pages 201-209, 2013. |
| [5] | Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms SPIN, volume 7976 of LNCS, pages 209-226, 2013. |
| [4] | Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction PODC, pages 119-121, 2013. |
| 2012 | |
| [3] | Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms ArXiv e-prints, October 2012. |
| [2] | Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms ArXiv e-prints, October 2012. |
| [1] | Who is afraid of Model Checking Distributed Algorithms? 2012, Presentation at the CAV Workshop (EC)^2. |
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: | ta.etysrofnull@vonnok |
| Web: | http://forsyte.at/~konnov/ |
