OCRA – Othello Contracts Refinement Analysis

OCRA is a tool for the verification of logic-based contracts refinement for embedded systems.

It supports the specification of components enriched with Othello contracts and the compositional verification of contracts refinement and implementation.

It is built on top of the NuSMV model checker.

We are glad to announce the availability of a new version of OCRA. OCRA version 1.1.2 is a bug fix release that provides some important bug fixes.

Contacts

Stefano Tonetta <>

Website