BMC4UML
is a (prototype) module of the verification system VerICS, aimed at verification of concurrent systems specified in a subset of UML 2.1, using the bounded model checking method. It is still in a preliminary stage and needs some improvements. However, some encouraging experimental results have been obtained (see publications list).Contrary to other verifiers for UML, we do not translate UML specifications to any intermediate representation, but encode directly all the possible computations of a UML system (unfolded to a given depth k) as a propositional formula. Then we check satisfiability of the conjuction of this formula and the formula which encodes a tested property. This is done using a SAT-solver.
Download:
At the moment BMC4UML is deployed only as VerICS' module.