User Manual

The user manual, providing the definition of the language and the documentation about the user commands, can be found here.

Related publications

  • SEFM 2016: Alessandro Cimatti, Ramiro Demasi, Stefano Tonetta: Tightening a Contract Refinement. SEFM 2016. Springer original.


  • SCP 2015: Alessandro Cimatti, Stefano Tonetta: Contracts-refinement proof system for component-based embedded systems. Journal Science of Computer Programming. 97: 333-348 (2015). Elsevier original. Manuscript.
  • ATVA 2014: Marco Bozzano, Alessandro Cimatti, Cristian Mattarei, Stefano Tonetta: Formal Safety Assessment via Contract-Based Design. ATVA 2014: 81-97. Springer original.


  • SAFECOMP 2014: Thomas Arts, Michele Dorigatti, Stefano Tonetta: Making Implicit Safety Requirements Explicit - An AUTOSAR Safety Case. SAFECOMP 2014: 81-92.

Springer original. Manuscript.

  • ASE 2013: Alessandro Cimatti, Michele Dorigatti, Stefano Tonetta: OCRA: A tool for checking the refinement of temporal contracts. ASE 2013: 702-705.

IEEE original. Manuscript.

  • SEAA 2012: Alessandro Cimatti, Stefano Tonetta: A Property-Based Proof System for Contract-Based Design. EUROMICRO-SEAA 2012: 21-28.

IEEE original. Manuscript.


  • ACVI 2016 Workshop. April 5, 2016 Venice, Italy (slides).


The slides and examples used during the tutorial presented at ASE 2013 can be found here.


See an old demonstration of the usage of the tool.