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 your software




Client since 2014: 4 years of licencing and support, 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?