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).
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“. The most recent and efficient techniques can be found in our CAV’15 paper (limited to reachability properties) and the draft of the submission accepted to POPL’17 (safety and liveness). A detailed exposition of the earlier techniques can be found in the tutorial given at SFM Summer School’14.
See the short list on the right or check the full archive.
||| 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.
||| On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability|
Inf. Comput., volume 252, pages 95-109, 2017.
||| 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
||| 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.
||| 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)
||| 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.
||| 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.
||| 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.
||| Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms|
Formal Methods for Executable Software Models, pages 122-171, 2014, Springer.
||| Parameterized model checking of fault-tolerant distributed algorithms by abstraction|
FMCAD, pages 201-209, 2013.
||| Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms|
SPIN, volume 7976 of LNCS, pages 209-226, 2013.
||| Brief announcement: parameterized model checking of fault-tolerant distributed algorithms by abstraction|
PODC, pages 119-121, 2013.
||| Starting a Dialog between Model Checking and Fault-tolerant Distributed Algorithms|
ArXiv e-prints, October 2012.
||| Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms|
ArXiv e-prints, October 2012.
||| Who is afraid of Model Checking Distributed Algorithms?|
2012, Presentation at the CAV Workshop (EC)^2.
Browse up-to-date benchmarks in the github repository.
Now available at github.
- 16.01.2017, ver. 2.2.0 Virtual machine (Debian 8u1 64-bit) improved after the POPL’17 artifact evalation: bymc-2.2.0-popl17-64bit.ova [1.6 GB]
- 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] (WARNING: very old version)
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.
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.
Technische Universität Wien
Institut für Informationssysteme 184/4
|Room:||HD 03 13 (how to get there)|
|Phone:||+43 (1) 58801 – 184 807|