High Integrity Lint Integrated with Testing and Execution
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 projects to combine different techniques around a common expression of properties and constraints. Hi-Lite's focus on modularity allows scaling to large software systems and encourages early adoption. By relying only on sound static analyses, Hi-Lite qualifies for being a tool of choice for industrial users needing to apply the Formal Methods Supplement of the upcoming DO-178C standard. Hi-Lite is completely based on free software. The project is structured as two different tool-chains for Ada and C based on GNAT/GCC compilers (Ada and C), the CodePeer static analyzer (Ada), the SPARK verification tool-set (Ada) and the Frama-C platform (C), all integrated inside AdaCore IDEs.

Number of scientific articles published: 0

The results of the Why3 project have been presented in 20 scientific and technical articles in international conferences or journals, 7 international communications,
and many gatherings with academics or industrial partners/prospects/customers.

Number of patents filed: 0

Number of product’s innovation: 3

Project Hi-Lite has had a major impact on the products developed by CEA and AdaCore for verifying software at the highest levels of criticality.
CEA has integrated in its flagship product Frama-C the ability to execute logical specifications.
AdaCore has completely replaced the existing SPARK technology with a new toolset based on the Why3 and Alt-Ergo software bricks from Inria.
Inria has also released a completely new implementation of their verification technology called Why3.

Number of product’s innovation service: 0

Number of projected jobs created: 0

Number of jobs maintained: 0

Number of related companies creation: 0