| CARVIEW |
Select Language
HTTP/2 200
server: nginx/1.24.0 (Ubuntu)
date: Fri, 16 Jan 2026 17:10:54 GMT
content-type: text/html
content-length: 1543
last-modified: Tue, 30 May 2023 08:13:01 GMT
etag: "dc0-5fce4c593a1f4-gzip"
accept-ranges: bytes
vary: Accept-Encoding
content-encoding: gzip
strict-transport-security: max-age=31536000; includeSubDomains
OCRA - Home page
Welcome
Welcome to the home page of OCRA, a command-line tool for the verification of logic-based contract refinement for embedded systems.
It supports the specification and analysis of component-based specifications of system architectures.
Components are enriched with contracts specified in discrete or hybrid linear-time temporal logics.
OCRA is developed by the Embedded Systems Unit of FBK.
It is built on top of the nuXmv and HyCOMP model checkers.
It is also integrated in the modeling tool AutoFOCUS3 through the AF3-OCRA plugin.
Latest release
7/02/2021
OCRA 2.1.0 is a major release that provides a new time domain.
Several bugs were also fixed.
More information here.
Download here .
Contact: ocra@fbk.eu