Project Hi-Lite

Hi-Lite is a project aiming at popularizing formal methods for the development of high-integrity software. It targets ease of adoption through a loose integration of formal proofs with testing and static analysis, that allows combining techniques around a common expression of specifications. Its technical focus is on modularity, that allows a divide-and-conquer approach to large software systems, as well as an early adoption by all programmers in the software life cycle.

Hi-Lite is completely based on libre software. The project is structured in two different toolchains for Ada and C based on GNAT/GCC compilers, the SPARK verification toolset and the Frama-C platform. The integration of these toolchains inside two industrial IDEs offers to the user a common interaction on Ada and C programs. In particular, mixed Ada/C programs can be verified against a common specification.

Project Hi-Lite has officially launched and we will be reporting on its progress here as it reaches major milestones throughout the evolution of the project.

To get started on Hi-Lite, see

• a high-level view of the research context of Hi-Lite (in French, but see anyway the diagrams on slides 3 and 23)
• a description of the industrial context of Hi-Lite
• the initial technical project description (in French)

A "Lighter" Introduction to Hi-Lite

Hi-Lite is based on powerful industrial tools that have been developed by the different partners for the last 10 to 25 years. In order to show you how Hi-Lite can improve on the existing state-of-the-art by creating new communications between these tools, we describe in the following the application of the various tools and techniques that are part of Hi-Lite to a very simple program.

For the full story: Click here »

Headlines

2012-07-13: the first GPL release of GNATprove is now available on Linux and Windows.

2012-summer: Ricardo Aguirre Reyes is doing a 3-month summer student project on Hi-Lite funded by European Space Agency.

2012-06-14: Yannick Moy presented the progress on Hi-Lite at a workshop on formal methods at IRILL in Paris, France.

2012-06-26 - 2012-07-01: Claire Dross presented the paper Reasoning with Triggers at the SMT workshop affiliated with IJCAR conference in Manchester, UK.

2012-07-26 - 2012-07-06: Yannick Moy participated in the Dagstuhl seminar AI meets Formal Software Development in Saarbrücken, Germany.

2012-08-27 - 2012-08-31: Virginia Aponte and Pierre Courtieu (CNAM researchers) will present the paper Maximal and Compositional Pattern-Based Loop Invariants at FM 2012 conference in Paris, France.

Related Initiatives

The Workshop on Theorem Proving in Certification is now organized as a recurring event to compare approaches and tools based on theorem proving to critical software (such as avionics software), where a certification standard applies (DO-178B/C for avionics software). Here is the 2010 workshop and the 2011 workshop.

The tool ImProve performs formal verification (via model checking) on a small Embedded Domain Specific Language inside Haskell, and code generation to C.

Funding

Hi-Lite is an Open Source project financially supported by the French Government and the Essone general council in an effort to increase the use of formal methods in developing high-integrity software, particularly to meet the forthcoming DO-178C avionics standard.

Partners

The project partners are AdaCore, Altran Praxis, Astrium Space Transportation, CEA-LIST, the ProVal team of INRIA and Thales Communications. AdaCore is the project leader.

For more information on partners: Hi-Lite Partners Page »

Videos

Hi-Lite: a Verification Toolkit for Unit Test & Unit Proof
A presentation by Yannick Moy, Senior Engineer, AdaCore, at a talk at IRILL Days 2010. Video courtesy of IRILL (www.irill.org)

An Introduction to Open DO
A presentation by Cyrille Comar, Managing director of AdaCore Europe

You can also view the presentation slides if you want to follow along. Note that the Hi-Lite slides start on page 30..

More Resources

For the latest news and events on Project Hi-Lite: Hi-Lite News and Events Page »

For the latest papers and presentations on Project Hi-Lite: Hi-Lite Resources Page »

To watch recent progress made in Project Hi-Lite: Hi-Lite Progress Page »

Get Involved

If you are interested in participating in the Hi-Lite effort: Open-DO Forge »

To participate in the technical discussions, subscribe to Hi-Lite mailing-list »

Contact

For more information about project Hi-Lite: info@open-do.org