Difference between revisions of "BPJ Model Checking"
From BP Wiki
| Line 1: | Line 1: | ||
| − | = Model Checking Behavioral Applications with BPmc | + | = Model Checking Behavioral Applications with BPmc= |
You can find bugs and underspecification in behavioral programs using model checking. | You can find bugs and underspecification in behavioral programs using model checking. | ||
Revision as of 13:52, 4 August 2013
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.
