Below are links for downloading the latest stable release of probcli (the command line version of ProB) and ProB Tcl/Tk (ProB with a graphical user interface written in Tcl/Tk). Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.
Details of the ProB Licence can be found here. ProB is free to use and open source. For commercial support contact the spin-off company Formal Mind or Michael Leuschel. In particular, we can provide access to the validation report for using ProB as a tool of class T2 or T3 within the European norm EN50128.
| Platform | Release Date | Download (64 bit) | Dependencies |
|---|---|---|---|
| 1.9.3-final | |||
| Linux | 19.2.2020 | Tarball |
Java Runtime Environment (7.0 or newer) or Adopt JDK, Tcl/Tk 8.5, GraphViz |
| Windows | 19.2.2020 | Zipfile (Tcl/Tk 8.6), Zipfile (Tcl/Tk 8.5) |
Tcl/Tk for Windows,
Java Runtime Environment (7.0 or newer) or Adopt JDK, |
| OS X | 19.2.2020 | Zipfile (notarized) |
OS X 10.9 (Mavericks) or newer, Tcl/TK 8.5 (e.g., 8.5.18.0),
Java Runtime Environment or better Java JDK or Adopt JDK, |
The B parser of ProB requires Java 7 or newer. Sometimes you have to install the Java JDK (and not the JRE) so that the new Java version becomes visible to command-line tools. The Graphical User Interface of ProB Tcl/Tk requires Tcl/Tk 8.5 unless stated otherwise. All releases include the command-line version probcli which does not require Tcl/Tk. All releases are compiled for 64-bit architectures. Note: If you wish to use ProB on Windows XP you need the service pack SP3 installed.
The latest beta release is 1.10.0-beta1. An official beta release always passes all of ProB's tests. However, we do not follow the stringent checklist for final releases (e.g., checking SICStus Prolog Spider warnings, checking coverage and additional manual UI tests). Also, we do not store coverage reports and other information necessary for T2 certification.
More current nightly integration releases are also available below. These releases are not stored and usually updated every night.
You can now create Jupyter Notebooks in B using the ProB Jupyter Kernel.
To install ProB for Rodin, first download Rodin 2.8, Rodin 3.3 or Rodin 3.4, choose Help -> Install New Software and simply choose the pre-configured ProB update site. (The pre-configured update site is http://www.stups.uni-duesseldorf.de/prob_updates for Rodin 2.8 and http://www.stups.hhu.de/prob_updates_rodin3 for Rodin 3.x. The update site for nightly builds for Rodin 3.x is https://www3.hhu.de/stups/rodin/prob1/nightly.) More detailed installation instructions and a brief tutorial are available.
Warning: in Rodin 3.4 there is an issue where a model checking counter example leads to a hanging Rodin if the machine is not initialised. The issue is solved in the latest nightly build of ProB for Rodin (https://www3.hhu.de/stups/rodin/prob1/nightly). The issue is not present in Rodin 3.3.
Version 1.0.0 and the snapshot of 1.0.1 of the new Java FX UI (aka ProB2 FX) is available at https://www3.hhu.de/stups/downloads/prob2/:
It is tested with Java 8. We recommend using Azul Zulu. Adopt OpenJDK does not come with JavaFX at the moment.
You can also start the latest version directly from source.
You can remove "--exclude-task createHelp" if you have pandoc installed.
With Java 11 or newer we currently recommend running ProB2-UI from source. Otherwise, you have to install JavaFX in addition to Java itself and start ProB2-UI using the command like the following (but the command is incomplete):
java --module-path ..../javafx-sdk-11.0.2/lib --add-modules=javafx.controls,javafx.fxml,javafx.base,javafx.graphics,javafx.swing,javafx.web -jar prob2-ui-1.0.0-all.jar
We also provide a plugin for SVG-based visualization called VisB at https://www3.hhu.de/stups/downloads/prob2/plugins/.
The underlying API ProB2 of ProB2UI is available to Java developers via Maven Central.
A VIM plugin for ProB is available. It shows a quick fix list of parse and type errors for classical B machines (.mch) using the command line tool probcli. VIM has builtin syntax highlighting support for B.
There is a package language-b-eventb available for the Atom editor. It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom. It integrates with command line tool probcli to obtain error markers for syntax and type errors.
Some BBedit Language modules for B, TLA+, CSP and Prolog are available; these do not use command line tool probcli.
Prior Versions of ProB going back to 1.3.1 are available for download here. If you are interested in still earlier releases, please have a look at the Download directory.
The B parser of ProB 1.5.1 requires Java Runtime Environment (JRE) 7 or newer. ProB 1.5.0 can be run with JRE 6. Note: on some systems (Mac OS X) you may have to install a JDK such as the Adopt OpenJDK, Azul Zulu or the Oracle JDK/JSE (and not just the JRE) so that Java 7 or 8 becomes available to the command-line tools (type java -version to check which version is used by default for command-line tools; see also this discussion on StackOverflow). In case you have trouble starting the Java parser you can now set the JAVA_PATH preference of ProB to point to the java tool (or java.exe on Windows).
To check whether ProB can correctly use its Java parser you can type the following (using probcli.exe on Windows):
probcli -version -v
This will try and start the parser and obtain the parser version. In case Java is not correctly installed you should get an error message. On Windows, you may see the error message
Error occurred during initialization of VM
on the console. This means you should probably re-install the Java JRE with admin rights and try again. If you see the error message
Unsupported major.minor version 51.0
this means you do not have Java 7 or newer installed. You can try setting the path to the correct java version by setting the JAVA_PATH preference as follows:
probcli -p JAVA_PATH path/to/java -version -v
ProB Tcl/Tk requires an installation of Tcl/Tk 8.5. The command-line tool probcli does not require this. Please note that Tcl/Tk 8.6 is not yet generally supported by SICStus Prolog (even though ProB may work with Tcl/Tk 8.6; we recommend installing Tcl/Tk 8.5 though).
Note: for Mac OS you may have to install the ActiveTcl version of Tcl/Tk (e.g., 8.5.18.0) as indicated above (the distribution provided by Apple is typically broken, e.g., after opening a file using the standard file selection dialog some versions crash). However, even the version of Active Tcl/Tk on Mac can be quite unreliable and prone to crashing; for example version 8.5.12 has a serious bug related to copying text, see also here). This issue has been fixed in version 8.5.13 or later.
Note: on macOS Catalina the Tcl/Tk menu bar is sometimes not working. Switching to another application and then back to ProB seems to solve the problem.
Starting with ProB 1.3.5 you can now use ProB with Tcl/Tk 8.5 on Windows. If you have the older version of Tcl/Tk 8.4 you have to install the newer one 8.5 (you should be able to also keep the older version). For Windows we recommend installing ActiveTcl-8.5 (e.g., 8.5.18.0). Note: For the 64 bit version of ProB for Windows, you have to install the 64 bit Tcl/Tk 8.5 version! If you wish to use ProB on Windows XP you need the service pack SP3 installed.
On Linux you can typically install Tcl/Tk using sudo apt-get install tcl8.5 tk8.5. On Linux OpenSuse (12.3) you may have to perform the following for ProB to work:
ln -s /usr/lib/libtk8.5.so /usr/lib/libtk8.5.so.0 ln -s /usr/lib/libtcl8.5.so /usr/lib/libtcl8.5.so.0
Also, some of the feature require the table extension, which can be installed like this:
sudo apt install tk-table
Finally, support for .png ANIMATION_IMG declarations requires the Img package:
sudo apt install libtk-img
If you wish to view various visualizations generated by ProB Tcl/Tk or probcli you will need GraphViz. ProB may use the command-line tool dot, a dot-file viewer such as dotty or more recently the command-line tool sfdp.
On Mac you can now install the latest version of Graphviz using brew:
1. brew uninstall graphviz 2. brew install graphviz --with-gts 3. brew link --overwrite graphviz
Step 1. is optional; you only need to use it if you have a prior version of Graphviz installed. Step3 links the binaries to /usr/local/bin. This is probably better than using the older version from Pixelglow.
Note: if you wish to use the fast rendering for large state spaces in ProB 1.7.x, you need the sfdp tool of GraphViz (ideally version 2.28 or newer with the triangulation library; when installing using brew use the option --with-gts; see the section below). ProB 1.8.1 only uses the dot binary, making use of the -Ksfdp option.
You can download the latest Prolog sourcecode snapshot from: http://www3.hhu.de/stups/downloads/prob/source/
The source code for the ProB parsers (B, LTL, ...) can be obtained from: https://github.com/hhu-stups/probparsers.
The ProB2-Java-API source code can be obtained from: https://github.com/hhu-stups/prob2_kernel.
The ProB2-Java-FX UI source code can be obtained from: https://github.com/hhu-stups/prob2_ui.
19/2/2020 ProB 1.9.3 is available. Highlights: performance improvements, new external functions, performance monitoring.
11/11/2019 ProB 1.9.2 is available. Minor bugfix release.
8/11/2019 ProB 1.9.1 is available. Maintenance release.
12/7/2019 ProB 1.9.0 is available. Highlights: improved error feedback, improved Unicode support, regular expression library, memoization.
1/10/2018 ProB 1.8.2 is available. Highlights: improved error feedback, support Jupyter kernel, first support for Alloy models.
20/03/2018 ProB 1.8.0 is available. Highlights: terminal colour support, performance improvements for displaying very large values, improved symmetry breaking and constraint solving.
5/10/2017 ProB 1.7.1 is available. Highlights: performance, non-deterministic assigned variables shown, Z improvements, export history to HTML.
11/7/2017 ProB 1.7.0 is available. Highlights: improved Latex document generation, improved XML/CSV data import and export, RULE DSL language, many improvements in constraint solver.
20/10/2016 ProB 1.6.1 is available. Highlights: Latex document generation, LET and IF-THEN-ELSE for expressions and predicates, XML logging, XML data import, performance improvements.
22/4/2016 ProB 1.6.0 is available. Highlights: directed model checking, Z3 available as backend, B line comments and unicode symbols, improved error messages, performance improvements.
19/2/2015 ProB 1.5.0 is available. Highlights: improved random enumeration, MACE/SEM style static symmetry reduction for deferred set elements, MC/DC coverage analysis for guards and invariants, improved TLC interface, bug fixes and improvements including but not limited to the constraint solver.
29/8/2014 ProB 1.4.1, a small bugfix-only release is available. For a list of new features in 1.4.0 see below.
18/8/2014 ProB 1.4.0 is available. Highlights: CLP(FD)-based constraint solver enabled by default, kernel can handle more operations symbolically, integration of the TLC model checker, bug fixes and performance improvements.
4/3/2013 ProB 1.3.6 is available. Highlights: improved constraint propagation for division, modulo, intervals, model checking progress bar, performance improvements, improved Kodkod backend and use within REPL, and many more.
8/10/2012 ProB 1.3.5 is available. Highlights: support for external and recursive functions, optional Kodkod backend, TLA+ support, performance improvements, pragmas, units inference, and many more.
30/03/2012 A first prototype of an online ProB Logic Calculator is available.
21/11/2011 ProB 1.3.4 is available. Highlights: Evaluation View and Eval window, CSP assertion checking, improved editor, 64-bit version for Mac and Linux, performance improvements, and many more.
10/02/2011 ProB 1.3.3 and ProB for Rodin 2.3 is available. Highlights: improved performance, constrained-based deadlock checking, record detection, and many more.
07/30/2010 ProB 1.3.2 is available. Highlights: improved performance, constraint solving over integers (enable in Advanced Preferences), much improved Z support, and many more.
12/07/2009 ProB 1.3.1 is available. Highlights: new data-structure for large sets and relations (see FM 2009), multi-level validation for Event-B, improved constraint propagation for boolean connectives, and many more.
03/20/2009 ProB 1.3.0 is available for download. Highlights: New parser and integrated typechecker, install as AtelierB plugin, improved kernel with support for large sets/relations, improved CSP support, faster LTL model checker, Undo/Redo in text editor, graphical formula viewer, user definable custom animations with gifs.
The full ProB release history can be found here.