• 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.
- Le pôle
- Ambition PME
- Les projets
- Europe / International
- Clip du projet IOLS
- Clip du projet URC