The French Institute for Radiological Protection and Nuclear Safety (IRSN) set up by law 2001-398 of 9 May 2001, under the statute of public authority of industrial and commercial nature (EPIC) is the national public expert in nuclear and radiological risks. IRSN contributes to public policy-making concerning nuclear safety and health and environmental protection against ionizing radiation. As a research and expert appraisal organization, IRSN works together with all the participants concerned by these policies while keeping an open mind.


French nuclear reactors rely heavily on software to perform critical safety tasks. Because of this, IRSN encourages the use of formal methods to prove the correctness of the software. This is crucial to ensure the proper performance of the required safety tasks. IRSN also actively participates in the improvement of tools and their associated analyses methodologies through activities carried out by both research labs and TrustInSoft.


To explore new approaches that prove different structural properties on critical safety C software, IRSN required an advanced and robust static analysis tool with a high level of reactive support. IRSN became an early adopter of the TrustInSoft Analyzer. They use a license on a dedicated computer to perform comprehensive formal verification on its C software.

icon benefits


Increased guarantees of correctness for critical software

Use of an effective tool & support to explore new approaches for proving structural properties, such as dependencies of software outputs

Efficient & professional support from expert developers with direct input and experience creating and implementing the analyzer

Compliance with IEC 60880

Application of formal methods to provide mathematical guarantees

Static Analysis framework with collaborating formal methods

Support for different architectures

Better understanding of all the behaviors of you




Client since 2014
One user
Analysis of 16 applicative software

software stats

Software Metrics

18 000 to 24 000 lines of code
230 to 270 functions


10 minutes to 1 hour

Additional code written in C

340 lines for a single analysis


Between 0 and a few dozen depending on the analyzed software

“TrustInSoft provides a highly advanced static analyzer along with a friendly GUI. Its efficient technical
support is a key point in the success of our software analyses. TrustInSoft helps us understand the
meaning of alarms raised, and provides customized solutions. These efforts are necessary to
understand the possibilities of the analyzer and the scope of the proven properties.”

Grégory de la Grange,
Engineer in Safety for Digital Instrumentation & Control, IRSN

Gregory de la grange IRSN

© Stéphanie Jayet/Médiathèque IRSN

Ready to learn more?