First MoWGLI Prototype

The prototype is accessible via a Web interface.

Validation: Smart Card Security

Mowgli's prototype was tested on the Java Card formal model, which contains more than 3750 formal definitions and 2000 theorems along 4MB of Coq source code. The intended purpose was to test Mowgli as a support for explaining those models to the evaluator.

Trusted Logic developed a tool for retrieving source information as meta-data. This includes several kinds of information that present in the sources but that is not part of logical terms, like comments on the formal definitions included in the source files, coercions, implicit arguments, derived constants, etc.

Download the meta-data extractor for CIC terms.

The second contribution that Trusted Logic developed is an SPM document of GlobalPlatform, a widely used card manager standard for smart cards.

Download the XML files containing the SPM document.

The third contribution that Trusted Logic developed is related to the use of Mowgli's XML output as an exchange format for formal models.

Download the sources of the translator from Coq to UML or look at some screen-shots of its output in Rational Rose [gp-comm.png, gp-install.png, tables-relations.png, tables.png].

Other Software

GtkMathView

GtkMathView is a GTK+ component for rendering MathML documents. The component can be customized as to react to user events such as clicking and selection.
The home page of the component, along with online documentation, dependencies, instructions for compilation, can be found here.

Hermes

Hermes is a content oriented LaTeX authoring tool for scientific articles; it converts the LaTeX source into XML with Content-MathML islands.
The home page of the converter, along with documentation and samples, can be found here.

This page is hosted by the Department of Computer Science, University of Bologna.
Last updated Fri Feb 2 17:12:19 CET 2007.