Software verification tool for Java as target language. Contract-based specification in OCL supported.