Matita Library

Scripts

The scripts used to generate the knowledge base of Matita can be browsed on line.

Large Developments

Freescale

The scripts present:

• an executable formalization of the operational semantics of any Freescale micro-controller of the HC05/HC08/RS08/HCS08 families
• a compiler from assembly language (pseudocodes + operands) to machine code
• several automatic checks for unhandled opcodes, memory accesses, correctness of ALU logic, etc.
• three examples of assembly programs (string reverse, counting sort and perfect numbers sieve) with sets of data to run them

The execution in the executable formalization has been compared to real world execution using the USB SPYDER08 in-circuit debugger.

The code (in OCaml) of an executable emulator, automatically generated from the scripts above. On the tests above, it runs at about 29% of the speed of the CodeWarrior emulation engine.

The formalization has been the Undergraduate Thesis of Mr. Cosimo Oliboni. The manuscript (italian only) can be found here.

The Formal System λδ (lambda-delta)

See the λδ home page.