​Flight control, nuclear reactor monitoring, and railway signaling software applications all share one key characteristic, which is that they are considered critical. So, they have to be bug-free and robust in terms of cybersecurity.

The verification tools used on critical software typically provide one of three answers: yes, the software is secure; no, the software is not secure; or the software is possibly not secure. In the event of a "maybe," these verification tools do provide a huge amount of information. The way the mass of information is presented, however, does not make it easy to interpret so that any bugs can be found. It is like looking for a needle in a haystack!

CEA-List researchers leveraged the institute's Frama-C code analysis software to develop Ivette. This new and scalable software environment will bring software verification engineers an improved user experience. Ivette's Web-3.0-inspired data mining and visualization technologies allow verification engineers to explore the results of an analysis in a relevant and interactive way. They can also fine tune the analyses themselves to increase the chances of getting a clear yes or no answer.

One of the main advantages offered by Ivette is that it is open source, so other code analysis tools can be integrated seamlessly for use with Frama-C. The high degree of interoperability also makes it easier to integrate Frama-C into industrial environments. The initial release has already been delivered to two major CEA-List partners. CEA-List researchers are already working on a new use case for Ivette: training for verification engineers and other experts.