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.
GtkMathView is a GTK+ component for rendering MathML documents. The
component can be customized as to react to user events such as clicking
Hermes is a content oriented LaTeX authoring tool for scientific articles;
it converts the LaTeX source into XML with Content-MathML islands.