LCERTIFY translation validator: A Library for Certification of Compilation

Xavier Rival

Principle

Static analysis techniques and analysis tools (such as Astrée) for the certification of safety critical softwares target the source code. However, if the compiler is not correct, this source level certification is not sound anymore. Thus, field specific regulations such as DO-178-B in avionics recommend target code be considered instead.

Alternatively, it is also possible to certify the compilation itself. There are several approaches to do that, in particular:

The Lcertify project investigates translation validation techniques, in the case of imperative language like C or user-specific languages with similar traits. The tool inputs a source program and a binary (Power-PC, Elf with 32-bits format, conforming to the Embedded ABI), performs an automatic computation that may produce two results:

Rather than a monolithic tool, it consists in a library-like system, which can be interfaced with various source front-ends (the same could be done for the binary front-end). Two front-ends were developped: a C front-end (conforming ANSI C), and a pseudo-code front-end, dedicated to a language used at Airbus (that development was part of the AsBaProd project).

Related projects

Related publications