Hi-Lite: a Verification Toolkit for Unit Test and Unit Proof

Until now, verification of safety-critical embedded programs has been relying mostly on tests. Costly code coverage objectives have been designed for these tests to achieve a reasonable level of confidence. The upcoming avionic standard DO-178C will allow one to replace tests with proofs, thus reaching higher levels of confidence at a lesser cost.
 
In order to benefit from this updated standard, aeronautic industries will need new development environments which include tools for proving program properties, which have been developed mostly in an academic setting until now. The goal of project Hi-Lite is to integrate existing verification tools (Verification Condition generator, automatic prover, static analyzer) inside industrial tool-chains (GUI, compiler, debugger) for Ada and C. Some of these tools are being developed by AdaCore and Altran Praxis companies, while others are developed by research labs at INRIA and CEA. All these tools are free software.
 
Free open-source software facilitates collaborations between teams that are expert on their own tools, in particular when academic research labs are involved. This mode of development partially fulfills a demand from industries which are anxious about finding expert support for long-lived projects. We also adopted a completely open development process for the new tools in Hi-Lite, with a public source forge, a public web-site for intermediate documents and a public mailing-list for discussing technical issues, which are all available from the Open-DO web-site.