17:1717:17, 16 March 2015diffhist+9,665 N
Tutorial Various Optimizations
Created page with '{{Revision}} The ordinary model checker of ProB enables the user to verify automatically whether a B model contains any errors such as deadlocks and invariant violations. The sea…'
15:4415:44, 12 January 2015diffhist+4,151 N
Mutual Exclusion (Fairness)
Created page with 'Consider an Event-B model formalizing an algorithm for mutual exclusion with semaphores for two concurrent processes <math>P_1</math> and <math>P_2</math>. Each process has been …'
17:2817:28, 6 November 2014diffhist+7,853 N
Tutorial LTL Counter-example View
Created page with 'In this tutorial a quick overview will be given describing the LTL counter-example visualization plug-in in Rodin. The functionality of the plug-in will be presented by means of …'