X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fmatita.shtml;h=0a331f58b03164190e5eb2705941d5cce5e8d976;hb=f336cc57864e1aebe9256240bf523fa5970d025a;hp=b06da9bd0b362bbd98e0c9e3fc10c6bc3547856e;hpb=b8e426e4d942b7776fe8411f01df6974b2d35fc5;p=helm.git diff --git a/helm/www/matita/matita.shtml b/helm/www/matita/matita.shtml index b06da9bd0..0a331f58b 100644 --- a/helm/www/matita/matita.shtml +++ b/helm/www/matita/matita.shtml @@ -28,13 +28,6 @@

- -

- - - Matita screenshot: authoring interface - -

An interactive prover is a software tool aiding the development of formal proofs by man-machine collaboration. It provides a formal language @@ -60,7 +53,7 @@ come equipped with proofs of (some of) their properties.

Matita is currently adopted in the European Union "Certified Complexity" Project - CerCo for the formal verification of a + CerCo 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.