Earlier this month, on March 3rd, AdaCore was awarded a grant by the French government and local authorities to develop an innovative set of tools integrated with its GNAT Pro platform. AdaCore is leading a consortium of 2 research institutes (CEA-List, the ProVal team of INRIA) and 4 industrial companies (AdaCore, Altran, Astrium and Thales Communications) in this effort. The project, named Hi-Lite, is starting in mid-2010 and will continue for 3 years.
Hi-Lite’s goal is to promote the use of formal methods in developing high-integrity software. It loosely integrates formal proofs with testing and static analysis, thus allowing developers to combine different techniques around a common expression of properties and constraints.
Hi-Lite is completely based on free software. The project is structured as two different toolchains for Ada and C based on GNAT/GCC compilers (Ada and C), the CodePeer static analyzer (Ada), the SPARK verification toolset (Ada) and the Frama-C platform (C).