Software Migrations Ltd [[http://www.smltd.com][Software Migrations Ltd]] (SML) use formal transformations to convert one form of code to another; they can work on anything from assembly language to high level requirements (e.g. Z specifications). They specialise in IBM assembler legacy systems, but also work with C and COBOL, and other languages. SML has translated over 25,000 assembler listing provided by different companies, with sizes of up to 28,000 lines of assembly code (most modules are smaller than that). They claim that about 90% of the work of migrations can be automated (depending on various factors). The services offered by this company are based on the FermaT technology developed in the 1980's and 1990's at the Universities of Oxford and Durham, and now at the Demontfort University. FermaT provides for mathematically proven code transformations which can be applied to programs written originally in assembly code or to compiler-generated code. The FermaT Transformation Engine is available for [[http://www.dur.ac.uk/martin.ward/fermat.html][downloading]]. Their Principal Consultant and author of FermaT is [[Martin Ward]]. CategoryCompany