The SyVOLT Contract Prover

SyVOLT is a contract prover for DSLTrans model transformations. It will guarantee that all inputs including the contract's pre-condition will produce outputs including the contract's post-condition.

Download SyVOLT here.

Here is a video describing SyVOLT.