It's ALIVEness

BPjs is now able to verify liveness properties, by marking sync points as "hot" (yes, that terminology is a tip of the hat to LSC's). BPjs can detect overall hot cycles (an infinite loop where a b-program, as a whole, must always advance even without external events) and b-thread specific cycles (where a b-thread is in an infinite loop where all it's sync points are "hot").

Also:

• Verification re-designed, so now it's possible to add new inspections and report new violations
• Easier to create a BProgram from multiple resources (based on actual user feedback!)
• BEvent sub classes assign a meaningful name by default to their instances (based on actual user feedback!!)
• Improvements to the documentation (both high-level and Javadocs, based on actual user feedback!!!).
• More tests (now over 81% coverage!*)

* We of course acknowledge that coverage itself is not enough, which is why we bother with verification in the first place. But it's not entirely useless either.