The ProB Animator and Model Checker - Revision history

David Geleßus at 17:20, 5 March 2026

2026-03-05T17:20:20Z

← Older revision		Revision as of 17:20, 5 March 2026
Line 14:		Line 14:
	Michael Leuschel and his group have won the first edition of the <b>[https://prologyear.logicprogramming.org/ColmerauerPrize.html Alain Colmerauer Prize]</b> for ProB.		Michael Leuschel and his group have won the first edition of the <b>[https://prologyear.logicprogramming.org/ColmerauerPrize.html Alain Colmerauer Prize]</b> for ProB.
	For commercial support contact [http://www.stups.uni-duesseldorf.de/~leuschel/ Michael Leuschel].		For commercial support contact [http://www.stups.uni-duesseldorf.de/~leuschel/ Michael Leuschel].


	=== Versions of ProB ===		=== Versions of ProB ===
Line 30:		Line 29:
	The core of ProB is implemented in [http://www.sics.se/isl/sicstuswww/site/index.html SICStus Prolog] (but can be run without a SICStus Prolog license). The ProB constraint solver is implemented using co-routining and the CLP(FD) finite domain library of SICStus. An alternate [[Using_ProB_with_KODKOD \| constraint solver based on Kodkod (and thus SAT)]] is also available within ProB, as is [[Using_ProB_with_Z3\|an integration with the SMT solver Z3]]. An alternate [[TLC\|model checking engine (using TLC)]] well-suited for lower level B specifications is available as is an integration with [https://github.com/utwente-fmt/ltsmin/releases LTSmin] as [[LTSmin\|model checking backend]].		The core of ProB is implemented in [http://www.sics.se/isl/sicstuswww/site/index.html SICStus Prolog] (but can be run without a SICStus Prolog license). The ProB constraint solver is implemented using co-routining and the CLP(FD) finite domain library of SICStus. An alternate [[Using_ProB_with_KODKOD \| constraint solver based on Kodkod (and thus SAT)]] is also available within ProB, as is [[Using_ProB_with_Z3\|an integration with the SMT solver Z3]]. An alternate [[TLC\|model checking engine (using TLC)]] well-suited for lower level B specifications is available as is an integration with [https://github.com/utwente-fmt/ltsmin/releases LTSmin] as [[LTSmin\|model checking backend]].
	The [[ProBLicence \| ProB Licence can be found here]].		The [[ProBLicence \| ProB Licence can be found here]].


	\|width="40%" style="background:#EDF2F2;padding:15px;" \| '''News'''		\|width="40%" style="background:#EDF2F2;padding:15px;" \| '''News'''
Line 83:		Line 81:
	'''2012-03-30''' [[ProB_Logic_Calculator\|ProB Logic Calculator]] available.		'''2012-03-30''' [[ProB_Logic_Calculator\|ProB Logic Calculator]] available.

	~~''' '''~~
	[[Download#Short Release History\|More in Release History]]		[[Download#Short Release History\|More in Release History]]
	\|}		\|}
Line 93:		Line 90:
	ProB supports also importing, validating and visualising [https://www.railml.org/en/applications/detail/prob.html railML data].		ProB supports also importing, validating and visualising [https://www.railml.org/en/applications/detail/prob.html railML data].

	[[File:ProBAtAGlance.png\| center \|500px]]		[[File:ProBAtAGlance.png\|center\|500px]]

	=== Citing ProB ===		=== Citing ProB ===
Line 103:		Line 100:
	* Michael Leuschel & Michael J. Butler (2008): ProB: an automated analysis toolset for the B method. STTT 10(2), pp. 185–203. Available at [http://dx.doi.org/10.1007/s10009-007-0063-9 http://dx.doi.org/10.1007/s10009-007-0063-9].		* Michael Leuschel & Michael J. Butler (2008): ProB: an automated analysis toolset for the B method. STTT 10(2), pp. 185–203. Available at [http://dx.doi.org/10.1007/s10009-007-0063-9 http://dx.doi.org/10.1007/s10009-007-0063-9].

	For convenience we also provide [[Citing ProB\|Bibtex entries for the above references]].		For convenience we also provide [[Citing ProB\|Bibtex entries for the above references]].


	__NOTOC__		__NOTOC__

David Geleßus: /* Versions of ProB */ Update links and simplify some wording

2026-03-05T17:18:06Z

Versions of ProB: Update links and simplify some wording

← Older revision		Revision as of 17:18, 5 March 2026
Line 20:		Line 20:
	Several versions of ProB are available. They all make use of the same Prolog core (see below).		Several versions of ProB are available. They all make use of the same Prolog core (see below).

	* A command-line tool called [[~~Using_the_Command~~-~~Line_Version_of_ProB~~\|probcli]]. It is distributed with the standard [[~~Download#Latest_Release\|~~download ~~of the latest release~~]].		* A command-line tool called [[Using the Command-Line Version of ProB\|probcli]]. It is distributed with the standard [[download]].
	* The original graphical user interface ProB Tcl/Tk. It is distributed with the standard [[~~Download#Latest_Release\|~~download ~~of the latest release~~]].		* The original graphical user interface ProB Tcl/Tk. It is distributed with the standard [[download]].
	* The ~~[[ProB2-UI\|~~new graphical user interface ProB2-UI]] based on ~~Java FX~~ and the ~~ProB2-~~Java-API ~~of ProB~~. It is available as a [[Download#~~ProB2_UI_using_Java_FX~~\| separate download]]. It contains [[VisB]] for SVG-based visualizations (as a successor to BMotionStudio).		* The new graphical user interface [[ProB2-UI]] based on JavaFX and the ProB Java API. It is available as a [[Download#ProB2-UI\|separate download]]. It contains [[VisB]] for SVG-based visualizations (as a successor to BMotionStudio).
	* [[~~ProB_for_Event~~-B\|ProB for use within Rodin]], the toolset for Event-B. It is [[Download#~~ProB_for_Rodin~~\|available as a plugin]].		* [[ProB for Event-B\|ProB for use within Rodin]], the toolset for Event-B. It is [[Download#ProB for Rodin\|available as a plugin]].
	* ~~An API for using ProB from Java, called~~ [[~~ProB_Java_API\|ProB2-~~Java-API]] (aka ~~ProB2~~). It is available via [https://~~search~~.~~maven~~.~~org~~/~~search?q=a:~~de.prob2.kernel Maven Central].		* The [[ProB Java API]] (aka "ProB 2 kernel") for using ProB from Java and other JVM languages. It is available via [https://central.sonatype.com/artifact/de.hhu.stups/de.prob2.kernel Maven Central].
	* A [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel kernel for Jupyter], allowing to use B and ProB from within Jupyter notebooks. It is available via [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel a seperate installation procedure].		* A [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel kernel for Jupyter], allowing to use B and ProB from within Jupyter notebooks. It is available via [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel a seperate installation procedure].



	=== Implementation ===		=== Implementation ===

Michael Leuschel at 09:38, 23 December 2025

2025-12-23T09:38:28Z

← Older revision		Revision as of 09:38, 23 December 2025
Line 36:		Line 36:
	\|width="40%" style="background:#EDF2F2;padding:15px;" \| '''News'''		\|width="40%" style="background:#EDF2F2;padding:15px;" \| '''News'''
	'''2025-12-21'''		'''2025-12-21'''
	[[Download\|ProB 1.15.1]] is available. Automatic use of operation reuse and compression~~. STORE_DETAILED_TRANSITION_INFOS preference~~. Interactive proof via animator interface for Rodin POs.		[[Download\|ProB 1.15.1]] is available. Automatic use of operation reuse and compression. Interactive proof via animator interface for Rodin POs.

	'''2025-06-26'''		'''2025-06-26'''
Line 42:		Line 42:

	'''2024-02-20'''		'''2024-02-20'''
	[[Download\|ProB 1.13.0]] is available. Better Rodin theory support. Template strings. READ_JSON and other ~~new~~ external functions. VisB support for groups and "use" element. [[Monte_Carlo_Tree_Search_Game_Play\|MCTS game play]].		[[Download\|ProB 1.13.0]] is available. Better Rodin theory support. Template strings. READ_JSON and other external functions. VisB support for groups and "use" element. [[Monte_Carlo_Tree_Search_Game_Play\|MCTS game play]].

	'''2023-08-10'''		'''2023-08-10'''
Line 57:		Line 57:

	'''2021-10-06'''		'''2021-10-06'''
	[[Download\|ProB 1.11.0]] is available. Improved support for infinite sets, operation caching, faster LTL checking ~~for~~ safety formulas, more compact .prob files, [[VisB\|VisB]] HTML export, constructive Z3 translation.		[[Download\|ProB 1.11.0]] is available. Improved support for infinite sets, operation caching, faster LTL checking of safety formulas, more compact .prob files, [[VisB\|VisB]] HTML export, constructive Z3 translation.

	'''2021-01-26'''		'''2021-01-26'''

Michael Leuschel at 09:36, 23 December 2025

2025-12-23T09:36:39Z

← Older revision		Revision as of 09:36, 23 December 2025
Line 54:		Line 54:

	'''2021-12-29'''		'''2021-12-29'''
	[[Download\|ProB 1.11.1]] is available. Identifiers between backquotes, flexible JSON trace replay, DPLLT solving~~, improvements to Z3 backend~~.		[[Download\|ProB 1.11.1]] is available. Identifiers between backquotes, flexible JSON trace replay, DPLLT solving.

	'''2021-10-06'''		'''2021-10-06'''
Line 63:		Line 63:

	'''2020-12-15'''		'''2020-12-15'''
	[[Download\|ProB 1.10.0]]. Highlights: [[Well-Definedness_Checking\|well-definedness prover]], [[Summary_of_B_Syntax#Reals:\|REAL datatype]], -lint comand for [[Editors_for_ProB#VSCode\|VSCode]] and [[Editors_for_ProB#Atom\|Atom]]~~, improved unsat core~~.		[[Download\|ProB 1.10.0]]. Highlights: [[Well-Definedness_Checking\|well-definedness prover]], [[Summary_of_B_Syntax#Reals:\|REAL datatype]], -lint comand for [[Editors_for_ProB#VSCode\|VSCode]] and [[Editors_for_ProB#Atom\|Atom]].

	'''2020-02-19'''		'''2020-02-19'''
Line 73:		Line 73:
	'''2018-10-01'''		'''2018-10-01'''
	[[Download\|ProB 1.8.2]]. Highlights: [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel Jupyter kernel], first [[Alloy\|support for Alloy models]].		[[Download\|ProB 1.8.2]]. Highlights: [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel Jupyter kernel], first [[Alloy\|support for Alloy models]].

	~~'''2017-07-11'''~~
	~~[[Download\|ProB 1.7.0]] Highlights: improved [[Generating_Documents_with_ProB_and_Latex \|Latex document generation]], improved XML/CSV support.~~

	'''2016-10-20'''		'''2016-10-20'''

Michael Leuschel at 09:35, 23 December 2025

2025-12-23T09:35:02Z

← Older revision		Revision as of 09:35, 23 December 2025
Line 35:		Line 35:

	\|width="40%" style="background:#EDF2F2;padding:15px;" \| '''News'''		\|width="40%" style="background:#EDF2F2;padding:15px;" \| '''News'''
	~~'''2024-02-20'''~~
	'''2025-12-21'''		'''2025-12-21'''
	[[Download\|ProB 1.15.1]] is available. Automatic use of operation reuse and compression ~~for model checking~~. STORE_DETAILED_TRANSITION_INFOS preference ~~and calls LTL property~~. Interactive proof via animator interface for Rodin ~~PO files~~.		[[Download\|ProB 1.15.1]] is available. Automatic use of operation reuse and compression. STORE_DETAILED_TRANSITION_INFOS preference. Interactive proof via animator interface for Rodin POs.

	'''2025-06-26'''		'''2025-06-26'''
	[[Download\|ProB 1.15.0]] is available. Interactive trace replay. Many [[VisB#VisB_DEFINITIONS \|VisB]] improvements ~~(use definition files for all models, grouping of VISB objects in a single definition, VISB_CLICK_META_INFOS, ...)~~. Profiling ~~can be turned on~~ via PROFILING_INFO preference.		[[Download\|ProB 1.15.0]] is available. Interactive trace replay. Many [[VisB#VisB_DEFINITIONS \|VisB]] improvements. Profiling via PROFILING_INFO preference.

			'''2024-02-20'''
	[[Download\|ProB 1.13.0]] is available. Better Rodin theory support. Template strings. READ_JSON and other new external functions. VisB support for groups and "use" element. [[Monte_Carlo_Tree_Search_Game_Play\|MCTS game play]].		[[Download\|ProB 1.13.0]] is available. Better Rodin theory support. Template strings. READ_JSON and other new external functions. VisB support for groups and "use" element. [[Monte_Carlo_Tree_Search_Game_Play\|MCTS game play]].

Michael Leuschel at 09:32, 23 December 2025

2025-12-23T09:32:58Z

← Older revision		Revision as of 09:32, 23 December 2025
Line 36:		Line 36:
	\|width="40%" style="background:#EDF2F2;padding:15px;" \| '''News'''		\|width="40%" style="background:#EDF2F2;padding:15px;" \| '''News'''
	'''2024-02-20'''		'''2024-02-20'''
			'''2025-12-21'''
			[[Download\|ProB 1.15.1]] is available. Automatic use of operation reuse and compression for model checking. STORE_DETAILED_TRANSITION_INFOS preference and calls LTL property. Interactive proof via animator interface for Rodin PO files.

			'''2025-06-26'''
			[[Download\|ProB 1.15.0]] is available. Interactive trace replay. Many [[VisB#VisB_DEFINITIONS \|VisB]] improvements (use definition files for all models, grouping of VISB objects in a single definition, VISB_CLICK_META_INFOS, ...). Profiling can be turned on via PROFILING_INFO preference.

	[[Download\|ProB 1.13.0]] is available. Better Rodin theory support. Template strings. READ_JSON and other new external functions. VisB support for groups and "use" element. [[Monte_Carlo_Tree_Search_Game_Play\|MCTS game play]].		[[Download\|ProB 1.13.0]] is available. Better Rodin theory support. Template strings. READ_JSON and other new external functions. VisB support for groups and "use" element. [[Monte_Carlo_Tree_Search_Game_Play\|MCTS game play]].

	'''2023-08-10'''		'''2023-08-10'''
	[[Download\|ProB 1.12.2]] is available. [[VisB#~~VisB_DEFINITIONS_2~~ \|VisB]] improvements.		[[Download\|ProB 1.12.2]] is available. [[VisB#VisB_DEFINITIONS \|VisB]] improvements.

	'''2023-04-04'''		'''2023-04-04'''

David Geleßus at 10:33, 20 February 2025

2025-02-20T10:33:01Z

← Older revision		Revision as of 10:33, 20 February 2025
Line 9:		Line 9:
	ProB can also be used as a [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel Jupyter kernel] to generate interactive notebooks.		ProB can also be used as a [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel Jupyter kernel] to generate interactive notebooks.

	ProB is being used within Alstom, ClearSy, Siemens, Thales and several other companies for [http://www.data-validation.fr data validation] of complicated properties for safety critical systems. It was used, e.g., for Paris ~~Line1~~, Sao Paulo line 4, Barcelona line 9 and many more.		ProB is being used within Alstom, ClearSy, Siemens, Thales and several other companies for [http://www.data-validation.fr data validation] of complicated properties for safety critical systems. It was used, e.g., for Paris Line 1, Sao Paulo line 4, Barcelona line 9 and many more.
	ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard for use at Thales.		ProB is certified T2 SIL4 according to the Cenelec EN 50128 standard for use at Thales.
	In this [https://www.youtube.com/watch?v=K6mS6akRmvA video from the Deutsche Bahn] you can see ProB animating a formal B model of the ETCS hybrid-level 3 principles in real-time, controlling two trains.		In this [https://www.youtube.com/watch?v=K6mS6akRmvA video from the Deutsche Bahn] you can see ProB animating a formal B model of the ETCS hybrid-level 3 principles in real-time, controlling two trains.
	Michael Leuschel and his group have won the first edition of the <b>[https://prologyear.logicprogramming.org/ColmerauerPrize.html ~~AlainColmerauer~~ Prize]</b> for ProB.		Michael Leuschel and his group have won the first edition of the <b>[https://prologyear.logicprogramming.org/ColmerauerPrize.html Alain Colmerauer Prize]</b> for ProB.
	For commercial support contact [http://www.stups.uni-duesseldorf.de/~leuschel/ Michael Leuschel].		For commercial support contact [http://www.stups.uni-duesseldorf.de/~leuschel/ Michael Leuschel].

Michael Leuschel: /* Features */

2024-08-16T12:12:50Z

Features

← Older revision		Revision as of 12:12, 16 August 2024
Line 90:		Line 90:
	ProB supports Z specifications (ProB in this context is sometimes called [[ProZ]]) as well as [[TLA\|TLA+ specifications]].		ProB supports Z specifications (ProB in this context is sometimes called [[ProZ]]) as well as [[TLA\|TLA+ specifications]].
	ProB can be used within Rodin and [http://www.atelierb.eu/en/ Atelier-B as a disprover and prover].		ProB can be used within Rodin and [http://www.atelierb.eu/en/ Atelier-B as a disprover and prover].
			ProB supports also importing, validating and visualising [https://www.railml.org/en/applications/detail/prob.html railML data].

	[[File:ProBAtAGlance.png\| center \|500px]]		[[File:ProBAtAGlance.png\| center \|500px]]

Michael Leuschel: /* Features */

2024-03-07T14:53:51Z

Features

← Older revision		Revision as of 14:53, 7 March 2024
Line 91:		Line 91:
	ProB can be used within Rodin and [http://www.atelierb.eu/en/ Atelier-B as a disprover and prover].		ProB can be used within Rodin and [http://www.atelierb.eu/en/ Atelier-B as a disprover and prover].

			[[File:ProBAtAGlance.png\| center \|500px]]
	[[File:ProBAtAGlance.png\|500px~~\|center~~]]

	=== Citing ProB ===		=== Citing ProB ===

Michael Leuschel: /* Features */

2024-03-07T14:52:14Z

Features

← Older revision		Revision as of 14:52, 7 March 2024
Line 92:		Line 92:


	[[File:ProBAtAGlance.png\|\|500px\|center]]		[[File:ProBAtAGlance.png\|500px\|center]]

	=== Citing ProB ===		=== Citing ProB ===