View source for BPJ Model Checking

= Model Checking Behavioral Applications with BPmc=

* You can find bugs and underspecification in behavioral programs using model checking.
* The BPmc model checker executes all possible paths of your program looking for states with desired and undesired properties per your specification.
* BPmc can check for safety  properties (including deadlocks) and for liveness  properties (with  fairness assumptions)
* [[Nondetermism | Nondeterministic execution in behavioral programming]]
* [[RunMode | Run mode specification for model-checking]] 
* State awareness
* Application Assistance