<p>
</p>
<!-- <a href="http://www.mkm-ig.org">Mathematical Knowledge Management</a> tools and techniques. </p> -->
-
- <p class="spaced">
- <span class="screenshots">
- <a class="quiet" href="images/screenshot-matita.png">
- <img src="images/MINI_screenshot-matita.png" alt="Matita screenshot: authoring interface" />
- </a>
- </span>
<p>An interactive prover is a software tool aiding the development of
formal proofs by man-machine collaboration. It provides a formal language
come equipped with proofs of (some of) their properties.</p>
<p>Matita is currently adopted in the European Union "Certified Complexity" Project
- <a href="http://cerco.cs.unibo.it/">CerCo<a> for the formal verification of a
+ <a href="http://cerco.cs.unibo.it/">CerCo</a> for the formal verification of a
complexity-preserving compiler from a large subset of C to a microcontroller
assembly of the kind traditionally used in embedded systems.
</p>