BPJ Model Checking

From BP Wiki
Revision as of 13:33, 4 August 2013 by Assaf (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

= 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.

  • [Nondetermism | Nondeterminisim in behavioral programming]]
Retrieved from "https://wiki.weizmann.ac.il/bp/index.php?title=BPJ_Model_Checking&oldid=32"